NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nchoicelem12 GIF version

Theorem nchoicelem12 6298
Description: Lemma for nchoice 6306. If the T-raising of a cardinal yields a finite special set, then so does the initial set. Theorem 7.1 of [Specker] p. 974. (Contributed by SF, 18-Mar-2015.)
Assertion
Ref Expression
nchoicelem12 ((M NC ( SpacTc M) Fin ) → ( SpacM) Fin )

Proof of Theorem nchoicelem12
Dummy variables m t x k n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 finnc 6242 . . . 4 (( SpacTc M) FinNc ( SpacTc M) Nn )
2 risset 2661 . . . 4 ( Nc ( SpacTc M) Nnx Nn x = Nc ( SpacTc M))
31, 2bitri 240 . . 3 (( SpacTc M) Finx Nn x = Nc ( SpacTc M))
4 nchoicelem11 6297 . . . . . . 7 {t m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn )} V
5 eqeq1 2359 . . . . . . . . 9 (t = 0c → (t = Nc ( SpacTc m) ↔ 0c = Nc ( SpacTc m)))
65imbi1d 308 . . . . . . . 8 (t = 0c → ((t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ (0c = Nc ( SpacTc m) → Nc ( Spacm) Nn )))
76ralbidv 2634 . . . . . . 7 (t = 0c → (m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ m NC (0c = Nc ( SpacTc m) → Nc ( Spacm) Nn )))
8 eqeq1 2359 . . . . . . . . 9 (t = n → (t = Nc ( SpacTc m) ↔ n = Nc ( SpacTc m)))
98imbi1d 308 . . . . . . . 8 (t = n → ((t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ (n = Nc ( SpacTc m) → Nc ( Spacm) Nn )))
109ralbidv 2634 . . . . . . 7 (t = n → (m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn )))
11 eqeq1 2359 . . . . . . . . . 10 (t = (n +c 1c) → (t = Nc ( SpacTc m) ↔ (n +c 1c) = Nc ( SpacTc m)))
1211imbi1d 308 . . . . . . . . 9 (t = (n +c 1c) → ((t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ ((n +c 1c) = Nc ( SpacTc m) → Nc ( Spacm) Nn )))
1312ralbidv 2634 . . . . . . . 8 (t = (n +c 1c) → (m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ m NC ((n +c 1c) = Nc ( SpacTc m) → Nc ( Spacm) Nn )))
14 tceq 6158 . . . . . . . . . . . . 13 (m = kTc m = Tc k)
1514fveq2d 5332 . . . . . . . . . . . 12 (m = k → ( SpacTc m) = ( SpacTc k))
1615nceqd 6110 . . . . . . . . . . 11 (m = kNc ( SpacTc m) = Nc ( SpacTc k))
1716eqeq2d 2364 . . . . . . . . . 10 (m = k → ((n +c 1c) = Nc ( SpacTc m) ↔ (n +c 1c) = Nc ( SpacTc k)))
18 fveq2 5328 . . . . . . . . . . . 12 (m = k → ( Spacm) = ( Spack))
1918nceqd 6110 . . . . . . . . . . 11 (m = kNc ( Spacm) = Nc ( Spack))
2019eleq1d 2419 . . . . . . . . . 10 (m = k → ( Nc ( Spacm) NnNc ( Spack) Nn ))
2117, 20imbi12d 311 . . . . . . . . 9 (m = k → (((n +c 1c) = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn )))
2221cbvralv 2835 . . . . . . . 8 (m NC ((n +c 1c) = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ k NC ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn ))
2313, 22syl6bb 252 . . . . . . 7 (t = (n +c 1c) → (m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ k NC ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn )))
24 eqeq1 2359 . . . . . . . . 9 (t = x → (t = Nc ( SpacTc m) ↔ x = Nc ( SpacTc m)))
2524imbi1d 308 . . . . . . . 8 (t = x → ((t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ (x = Nc ( SpacTc m) → Nc ( Spacm) Nn )))
2625ralbidv 2634 . . . . . . 7 (t = x → (m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ m NC (x = Nc ( SpacTc m) → Nc ( Spacm) Nn )))
27 tccl 6160 . . . . . . . . . . . . 13 (m NCTc m NC )
28 te0c 6236 . . . . . . . . . . . . 13 (m NC → ( Tc mc 0c) NC )
29 nchoicelem7 6293 . . . . . . . . . . . . 13 (( Tc m NC ( Tc mc 0c) NC ) → Nc ( SpacTc m) = ( Nc ( Spac ‘(2cc Tc m)) +c 1c))
3027, 28, 29syl2anc 642 . . . . . . . . . . . 12 (m NCNc ( SpacTc m) = ( Nc ( Spac ‘(2cc Tc m)) +c 1c))
31 0cnsuc 4401 . . . . . . . . . . . . 13 ( Nc ( Spac ‘(2cc Tc m)) +c 1c) ≠ 0c
3231a1i 10 . . . . . . . . . . . 12 (m NC → ( Nc ( Spac ‘(2cc Tc m)) +c 1c) ≠ 0c)
3330, 32eqnetrd 2534 . . . . . . . . . . 11 (m NCNc ( SpacTc m) ≠ 0c)
3433necomd 2599 . . . . . . . . . 10 (m NC → 0cNc ( SpacTc m))
35 df-ne 2518 . . . . . . . . . 10 (0cNc ( SpacTc m) ↔ ¬ 0c = Nc ( SpacTc m))
3634, 35sylib 188 . . . . . . . . 9 (m NC → ¬ 0c = Nc ( SpacTc m))
3736pm2.21d 98 . . . . . . . 8 (m NC → (0c = Nc ( SpacTc m) → Nc ( Spacm) Nn ))
3837rgen 2679 . . . . . . 7 m NC (0c = Nc ( SpacTc m) → Nc ( Spacm) Nn )
39 2nnc 6167 . . . . . . . . . . . . . . . . 17 2c Nn
40 ceclnn1 6189 . . . . . . . . . . . . . . . . 17 ((2c Nn k NC (kc 0c) NC ) → (2cc k) NC )
4139, 40mp3an1 1264 . . . . . . . . . . . . . . . 16 ((k NC (kc 0c) NC ) → (2cc k) NC )
42 tceq 6158 . . . . . . . . . . . . . . . . . . . . 21 (m = (2cc k) → Tc m = Tc (2cc k))
4342fveq2d 5332 . . . . . . . . . . . . . . . . . . . 20 (m = (2cc k) → ( SpacTc m) = ( SpacTc (2cc k)))
4443nceqd 6110 . . . . . . . . . . . . . . . . . . 19 (m = (2cc k) → Nc ( SpacTc m) = Nc ( SpacTc (2cc k)))
4544eqeq2d 2364 . . . . . . . . . . . . . . . . . 18 (m = (2cc k) → (n = Nc ( SpacTc m) ↔ n = Nc ( SpacTc (2cc k))))
46 fveq2 5328 . . . . . . . . . . . . . . . . . . . 20 (m = (2cc k) → ( Spacm) = ( Spac ‘(2cc k)))
4746nceqd 6110 . . . . . . . . . . . . . . . . . . 19 (m = (2cc k) → Nc ( Spacm) = Nc ( Spac ‘(2cc k)))
4847eleq1d 2419 . . . . . . . . . . . . . . . . . 18 (m = (2cc k) → ( Nc ( Spacm) NnNc ( Spac ‘(2cc k)) Nn ))
4945, 48imbi12d 311 . . . . . . . . . . . . . . . . 17 (m = (2cc k) → ((n = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )))
5049rspcv 2951 . . . . . . . . . . . . . . . 16 ((2cc k) NC → (m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn ) → (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )))
5141, 50syl 15 . . . . . . . . . . . . . . 15 ((k NC (kc 0c) NC ) → (m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn ) → (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )))
5251ancoms 439 . . . . . . . . . . . . . 14 (((kc 0c) NC k NC ) → (m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn ) → (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )))
5352adantrl 696 . . . . . . . . . . . . 13 (((kc 0c) NC (n Nn k NC )) → (m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn ) → (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )))
54 tccl 6160 . . . . . . . . . . . . . . . . . . . . . . 23 (k NCTc k NC )
55 te0c 6236 . . . . . . . . . . . . . . . . . . . . . . 23 (k NC → ( Tc kc 0c) NC )
56 nchoicelem7 6293 . . . . . . . . . . . . . . . . . . . . . . 23 (( Tc k NC ( Tc kc 0c) NC ) → Nc ( SpacTc k) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c))
5754, 55, 56syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22 (k NCNc ( SpacTc k) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c))
5857adantl 452 . . . . . . . . . . . . . . . . . . . . 21 ((n Nn k NC ) → Nc ( SpacTc k) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c))
5958adantl 452 . . . . . . . . . . . . . . . . . . . 20 (((kc 0c) NC (n Nn k NC )) → Nc ( SpacTc k) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c))
6059eqeq2d 2364 . . . . . . . . . . . . . . . . . . 19 (((kc 0c) NC (n Nn k NC )) → ((n +c 1c) = Nc ( SpacTc k) ↔ (n +c 1c) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c)))
61 nnnc 6146 . . . . . . . . . . . . . . . . . . . . . . 23 (n Nnn NC )
6261adantr 451 . . . . . . . . . . . . . . . . . . . . . 22 ((n Nn k NC ) → n NC )
6362adantl 452 . . . . . . . . . . . . . . . . . . . . 21 (((kc 0c) NC (n Nn k NC )) → n NC )
64 fvex 5339 . . . . . . . . . . . . . . . . . . . . . 22 ( Spac ‘(2cc Tc k)) V
6564ncelncsi 6121 . . . . . . . . . . . . . . . . . . . . 21 Nc ( Spac ‘(2cc Tc k)) NC
66 peano4nc 6150 . . . . . . . . . . . . . . . . . . . . 21 ((n NC Nc ( Spac ‘(2cc Tc k)) NC ) → ((n +c 1c) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c) ↔ n = Nc ( Spac ‘(2cc Tc k))))
6763, 65, 66sylancl 643 . . . . . . . . . . . . . . . . . . . 20 (((kc 0c) NC (n Nn k NC )) → ((n +c 1c) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c) ↔ n = Nc ( Spac ‘(2cc Tc k))))
68 tce2 6235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((k NC (kc 0c) NC ) → Tc (2cc k) = (2cc Tc k))
6968ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((kc 0c) NC k NC ) → Tc (2cc k) = (2cc Tc k))
7069adantrl 696 . . . . . . . . . . . . . . . . . . . . . . . 24 (((kc 0c) NC (n Nn k NC )) → Tc (2cc k) = (2cc Tc k))
7170fveq2d 5332 . . . . . . . . . . . . . . . . . . . . . . 23 (((kc 0c) NC (n Nn k NC )) → ( SpacTc (2cc k)) = ( Spac ‘(2cc Tc k)))
7271nceqd 6110 . . . . . . . . . . . . . . . . . . . . . 22 (((kc 0c) NC (n Nn k NC )) → Nc ( SpacTc (2cc k)) = Nc ( Spac ‘(2cc Tc k)))
7372eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 (((kc 0c) NC (n Nn k NC )) → (n = Nc ( SpacTc (2cc k)) ↔ n = Nc ( Spac ‘(2cc Tc k))))
7473biimprd 214 . . . . . . . . . . . . . . . . . . . 20 (((kc 0c) NC (n Nn k NC )) → (n = Nc ( Spac ‘(2cc Tc k)) → n = Nc ( SpacTc (2cc k))))
7567, 74sylbid 206 . . . . . . . . . . . . . . . . . . 19 (((kc 0c) NC (n Nn k NC )) → ((n +c 1c) = ( Nc ( Spac ‘(2cc Tc k)) +c 1c) → n = Nc ( SpacTc (2cc k))))
7660, 75sylbid 206 . . . . . . . . . . . . . . . . . 18 (((kc 0c) NC (n Nn k NC )) → ((n +c 1c) = Nc ( SpacTc k) → n = Nc ( SpacTc (2cc k))))
7776imim1d 69 . . . . . . . . . . . . . . . . 17 (((kc 0c) NC (n Nn k NC )) → ((n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn ) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spac ‘(2cc k)) Nn )))
7877imp 418 . . . . . . . . . . . . . . . 16 ((((kc 0c) NC (n Nn k NC )) (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spac ‘(2cc k)) Nn ))
79 peano2 4403 . . . . . . . . . . . . . . . 16 ( Nc ( Spac ‘(2cc k)) Nn → ( Nc ( Spac ‘(2cc k)) +c 1c) Nn )
8078, 79syl6 29 . . . . . . . . . . . . . . 15 ((((kc 0c) NC (n Nn k NC )) (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )) → ((n +c 1c) = Nc ( SpacTc k) → ( Nc ( Spac ‘(2cc k)) +c 1c) Nn ))
81 nchoicelem7 6293 . . . . . . . . . . . . . . . . . . 19 ((k NC (kc 0c) NC ) → Nc ( Spack) = ( Nc ( Spac ‘(2cc k)) +c 1c))
8281ancoms 439 . . . . . . . . . . . . . . . . . 18 (((kc 0c) NC k NC ) → Nc ( Spack) = ( Nc ( Spac ‘(2cc k)) +c 1c))
8382adantrl 696 . . . . . . . . . . . . . . . . 17 (((kc 0c) NC (n Nn k NC )) → Nc ( Spack) = ( Nc ( Spac ‘(2cc k)) +c 1c))
8483adantr 451 . . . . . . . . . . . . . . . 16 ((((kc 0c) NC (n Nn k NC )) (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )) → Nc ( Spack) = ( Nc ( Spac ‘(2cc k)) +c 1c))
8584eleq1d 2419 . . . . . . . . . . . . . . 15 ((((kc 0c) NC (n Nn k NC )) (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )) → ( Nc ( Spack) Nn ↔ ( Nc ( Spac ‘(2cc k)) +c 1c) Nn ))
8680, 85sylibrd 225 . . . . . . . . . . . . . 14 ((((kc 0c) NC (n Nn k NC )) (n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn )) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn ))
8786ex 423 . . . . . . . . . . . . 13 (((kc 0c) NC (n Nn k NC )) → ((n = Nc ( SpacTc (2cc k)) → Nc ( Spac ‘(2cc k)) Nn ) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn )))
8853, 87syld 40 . . . . . . . . . . . 12 (((kc 0c) NC (n Nn k NC )) → (m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn ) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn )))
8988expimpd 586 . . . . . . . . . . 11 ((kc 0c) NC → (((n Nn k NC ) m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn )) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn )))
90 nchoicelem3 6289 . . . . . . . . . . . . . . . . 17 ((k NC ¬ (kc 0c) NC ) → ( Spack) = {k})
9190nceqd 6110 . . . . . . . . . . . . . . . 16 ((k NC ¬ (kc 0c) NC ) → Nc ( Spack) = Nc {k})
92 vex 2862 . . . . . . . . . . . . . . . . . 18 k V
9392df1c3 6140 . . . . . . . . . . . . . . . . 17 1c = Nc {k}
94 1cnnc 4408 . . . . . . . . . . . . . . . . 17 1c Nn
9593, 94eqeltrri 2424 . . . . . . . . . . . . . . . 16 Nc {k} Nn
9691, 95syl6eqel 2441 . . . . . . . . . . . . . . 15 ((k NC ¬ (kc 0c) NC ) → Nc ( Spack) Nn )
9796a1d 22 . . . . . . . . . . . . . 14 ((k NC ¬ (kc 0c) NC ) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn ))
9897expcom 424 . . . . . . . . . . . . 13 (¬ (kc 0c) NC → (k NC → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn )))
9998adantld 453 . . . . . . . . . . . 12 (¬ (kc 0c) NC → ((n Nn k NC ) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn )))
10099adantrd 454 . . . . . . . . . . 11 (¬ (kc 0c) NC → (((n Nn k NC ) m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn )) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn )))
10189, 100pm2.61i 156 . . . . . . . . . 10 (((n Nn k NC ) m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn )) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn ))
102101an32s 779 . . . . . . . . 9 (((n Nn m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn )) k NC ) → ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn ))
103102ralrimiva 2697 . . . . . . . 8 ((n Nn m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn )) → k NC ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn ))
104103ex 423 . . . . . . 7 (n Nn → (m NC (n = Nc ( SpacTc m) → Nc ( Spacm) Nn ) → k NC ((n +c 1c) = Nc ( SpacTc k) → Nc ( Spack) Nn )))
1054, 7, 10, 23, 26, 38, 104finds 4411 . . . . . 6 (x Nnm NC (x = Nc ( SpacTc m) → Nc ( Spacm) Nn ))
106 tceq 6158 . . . . . . . . . . 11 (m = MTc m = Tc M)
107106fveq2d 5332 . . . . . . . . . 10 (m = M → ( SpacTc m) = ( SpacTc M))
108107nceqd 6110 . . . . . . . . 9 (m = MNc ( SpacTc m) = Nc ( SpacTc M))
109108eqeq2d 2364 . . . . . . . 8 (m = M → (x = Nc ( SpacTc m) ↔ x = Nc ( SpacTc M)))
110 fveq2 5328 . . . . . . . . . . 11 (m = M → ( Spacm) = ( SpacM))
111110nceqd 6110 . . . . . . . . . 10 (m = MNc ( Spacm) = Nc ( SpacM))
112111eleq1d 2419 . . . . . . . . 9 (m = M → ( Nc ( Spacm) NnNc ( SpacM) Nn ))
113 finnc 6242 . . . . . . . . 9 (( SpacM) FinNc ( SpacM) Nn )
114112, 113syl6bbr 254 . . . . . . . 8 (m = M → ( Nc ( Spacm) Nn ↔ ( SpacM) Fin ))
115109, 114imbi12d 311 . . . . . . 7 (m = M → ((x = Nc ( SpacTc m) → Nc ( Spacm) Nn ) ↔ (x = Nc ( SpacTc M) → ( SpacM) Fin )))
116115rspccv 2952 . . . . . 6 (m NC (x = Nc ( SpacTc m) → Nc ( Spacm) Nn ) → (M NC → (x = Nc ( SpacTc M) → ( SpacM) Fin )))
117105, 116syl 15 . . . . 5 (x Nn → (M NC → (x = Nc ( SpacTc M) → ( SpacM) Fin )))
118117com23 72 . . . 4 (x Nn → (x = Nc ( SpacTc M) → (M NC → ( SpacM) Fin )))
119118rexlimiv 2732 . . 3 (x Nn x = Nc ( SpacTc M) → (M NC → ( SpacM) Fin ))
1203, 119sylbi 187 . 2 (( SpacTc M) Fin → (M NC → ( SpacM) Fin ))
121120impcom 419 1 ((M NC ( SpacTc M) Fin ) → ( SpacM) Fin )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wa 358   = wceq 1642   wcel 1710  wne 2516  wral 2614  wrex 2615  {csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   Fin cfin 4376  cfv 4781  (class class class)co 5525   NC cncs 6088   Nc cnc 6091   Tc ctc 6093  2cc2c 6094  c cce 6096   Spac cspac 6271
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-fv 4795  df-2nd 4797  df-ov 5526  df-oprab 5528  df-mpt 5652  df-mpt2 5654  df-txp 5736  df-fix 5740  df-compose 5748  df-ins2 5750  df-ins3 5752  df-image 5754  df-ins4 5756  df-si3 5758  df-funs 5760  df-fns 5762  df-pw1fn 5766  df-fullfun 5768  df-clos1 5873  df-trans 5899  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-map 6001  df-en 6029  df-ncs 6098  df-lec 6099  df-ltc 6100  df-nc 6101  df-tc 6103  df-2c 6104  df-ce 6106  df-tcfn 6107  df-spac 6272
This theorem is referenced by:  nchoicelem19  6305
  Copyright terms: Public domain W3C validator