NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nnadjoin Structured version   Unicode version

Theorem nnadjoin 4520
Description: Adjoining a new element to every member of does not change its size. Theorem X.1.39 of [Rosser] p. 530. (Contributed by SF, 29-Jan-2015.)
Assertion
Ref Expression
nnadjoin Nn
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem nnadjoin
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sneq 3744 . . . . . . . . . . 11
21uneq2d 3418 . . . . . . . . . 10
32eqeq2d 2364 . . . . . . . . 9
43rexbidv 2635 . . . . . . . 8
54abbidv 2467 . . . . . . 7
65eleq1d 2419 . . . . . 6
76imbi2d 307 . . . . 5
87imbi2d 307 . . . 4 Nn Nn
9 nnadjoinlem1 4519 . . . . . . 7
10 eleq2 2414 . . . . . . . . . . 11 0c 0c
11 el0c 4420 . . . . . . . . . . . 12 0c
12 ab0 3569 . . . . . . . . . . . 12
1311, 12bitri 240 . . . . . . . . . . 11 0c
1410, 13syl6bb 252 . . . . . . . . . 10 0c
1514imbi2d 307 . . . . . . . . 9 0c
1615raleqbi1dv 2815 . . . . . . . 8 0c 0c
17 df-ral 2619 . . . . . . . . 9 0c 0c
18 el0c 4420 . . . . . . . . . . 11 0c
1918imbi1i 315 . . . . . . . . . 10 0c
2019albii 1566 . . . . . . . . 9 0c
21 0ex 4110 . . . . . . . . . 10
22 unieq 3900 . . . . . . . . . . . . 13
2322compleqd 3245 . . . . . . . . . . . 12
2423eleq2d 2420 . . . . . . . . . . 11
25 rexeq 2808 . . . . . . . . . . . . 13
2625notbid 285 . . . . . . . . . . . 12
2726albidv 1625 . . . . . . . . . . 11
2824, 27imbi12d 311 . . . . . . . . . 10
2921, 28ceqsalv 2885 . . . . . . . . 9
3017, 20, 293bitrri 263 . . . . . . . 8 0c
3116, 30syl6bbr 254 . . . . . . 7 0c
32 eleq2 2414 . . . . . . . . 9
3332imbi2d 307 . . . . . . . 8
3433raleqbi1dv 2815 . . . . . . 7
35 eleq2 2414 . . . . . . . . . 10 1c 1c
3635imbi2d 307 . . . . . . . . 9 1c 1c
3736raleqbi1dv 2815 . . . . . . . 8 1c 1c 1c
38 unieq 3900 . . . . . . . . . . . 12
3938compleqd 3245 . . . . . . . . . . 11
4039eleq2d 2420 . . . . . . . . . 10
41 rexeq 2808 . . . . . . . . . . . 12
4241abbidv 2467 . . . . . . . . . . 11
4342eleq1d 2419 . . . . . . . . . 10 1c 1c
4440, 43imbi12d 311 . . . . . . . . 9 1c 1c
4544cbvralv 2835 . . . . . . . 8 1c 1c 1c 1c
4637, 45syl6bb 252 . . . . . . 7 1c 1c 1c
47 eleq2 2414 . . . . . . . . 9
4847imbi2d 307 . . . . . . . 8
4948raleqbi1dv 2815 . . . . . . 7
50 rex0 3563 . . . . . . . . 9
5150ax-gen 1546 . . . . . . . 8
5251a1i 10 . . . . . . 7
53 elsuc 4412 . . . . . . . . . 10 1c
54 unieq 3900 . . . . . . . . . . . . . . . . . . . . 21
5554compleqd 3245 . . . . . . . . . . . . . . . . . . . 20
5655eleq2d 2420 . . . . . . . . . . . . . . . . . . 19
57 rexeq 2808 . . . . . . . . . . . . . . . . . . . . 21
5857abbidv 2467 . . . . . . . . . . . . . . . . . . . 20
5958eleq1d 2419 . . . . . . . . . . . . . . . . . . 19
6056, 59imbi12d 311 . . . . . . . . . . . . . . . . . 18
6160rspcv 2951 . . . . . . . . . . . . . . . . 17
6261adantr 451 . . . . . . . . . . . . . . . 16
6362adantl 452 . . . . . . . . . . . . . . 15 Nn
64 elin 3219 . . . . . . . . . . . . . . . . 17
65 simp3l 983 . . . . . . . . . . . . . . . . . . 19 Nn
66 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24
6766unisn 3907 . . . . . . . . . . . . . . . . . . . . . . 23
6867compleqi 3244 . . . . . . . . . . . . . . . . . . . . . 22
6968eleq2i 2417 . . . . . . . . . . . . . . . . . . . . 21
7069anbi2i 675 . . . . . . . . . . . . . . . . . . . 20
71 simpr 447 . . . . . . . . . . . . . . . . . . . . . 22 Nn
72 simpl2r 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Nn
7366elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7472, 73sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn
75 eleq1a 2422 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7675adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn
7774, 76mtod 168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn
78 simpl3r 1011 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Nn
79 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8079elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8178, 80sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn
82 simp3l 983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Nn
8379elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8482, 83sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Nn
85 elunii 3896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8685expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8786con3d 125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8884, 87mpan9 455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn
89 adj11 3889 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9081, 88, 89syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn
9177, 90mtbird 292 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nn
9291nrexdv 2717 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn
93 eqeq1 2359 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9493rexbidv 2635 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9594elabg 2986 . . . . . . . . . . . . . . . . . . . . . . . . 25
9695ibi 232 . . . . . . . . . . . . . . . . . . . . . . . 24
9792, 96nsyl 113 . . . . . . . . . . . . . . . . . . . . . . 23 Nn
9897adantr 451 . . . . . . . . . . . . . . . . . . . . . 22 Nn
99 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24
10066, 99unex 4106 . . . . . . . . . . . . . . . . . . . . . . 23
101100elsuci 4413 . . . . . . . . . . . . . . . . . . . . . 22 1c
10271, 98, 101syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21 Nn 1c
103102ex 423 . . . . . . . . . . . . . . . . . . . 20 Nn 1c
10470, 103syl3an3b 1220 . . . . . . . . . . . . . . . . . . 19 Nn 1c
10565, 104embantd 50 . . . . . . . . . . . . . . . . . 18 Nn 1c
1061053expia 1153 . . . . . . . . . . . . . . . . 17 Nn 1c
10764, 106syl5bi 208 . . . . . . . . . . . . . . . 16 Nn 1c
108107com23 72 . . . . . . . . . . . . . . 15 Nn 1c
10963, 108syld 40 . . . . . . . . . . . . . 14 Nn 1c
110109imp 418 . . . . . . . . . . . . 13 Nn 1c
111110an32s 779 . . . . . . . . . . . 12 Nn 1c
112 unieq 3900 . . . . . . . . . . . . . . . 16
113112compleqd 3245 . . . . . . . . . . . . . . 15
114 uniun 3910 . . . . . . . . . . . . . . . . 17
115114compleqi 3244 . . . . . . . . . . . . . . . 16
116 iunin 3547 . . . . . . . . . . . . . . . 16
117115, 116eqtri 2373 . . . . . . . . . . . . . . 15
118113, 117syl6eq 2401 . . . . . . . . . . . . . 14
119118eleq2d 2420 . . . . . . . . . . . . 13
120 rexeq 2808 . . . . . . . . . . . . . . . 16
121120abbidv 2467 . . . . . . . . . . . . . . 15
122 unab 3521 . . . . . . . . . . . . . . . 16
123 df-sn 3741 . . . . . . . . . . . . . . . . 17
124123uneq2i 3415 . . . . . . . . . . . . . . . 16
125 rexun 3443 . . . . . . . . . . . . . . . . . 18
126 uneq1 3411 . . . . . . . . . . . . . . . . . . . . 21
127126eqeq2d 2364 . . . . . . . . . . . . . . . . . . . 20
12866, 127rexsn 3768 . . . . . . . . . . . . . . . . . . 19
129128orbi2i 505 . . . . . . . . . . . . . . . . . 18
130125, 129bitri 240 . . . . . . . . . . . . . . . . 17
131130abbii 2465 . . . . . . . . . . . . . . . 16
132122, 124, 1313eqtr4ri 2384 . . . . . . . . . . . . . . 15
133121, 132syl6eq 2401 . . . . . . . . . . . . . 14
134133eleq1d 2419 . . . . . . . . . . . . 13 1c 1c
135119, 134imbi12d 311 . . . . . . . . . . . 12 1c 1c
136111, 135syl5ibrcom 213 . . . . . . . . . . 11 Nn 1c
137136rexlimdvva 2745 . . . . . . . . . 10 Nn 1c
13853, 137syl5bi 208 . . . . . . . . 9 Nn 1c 1c
139138ralrimiv 2696 . . . . . . . 8 Nn 1c 1c
140139ex 423 . . . . . . 7 Nn 1c 1c
1419, 31, 34, 46, 49, 52, 140finds 4410 . . . . . 6 Nn
142 unieq 3900 . . . . . . . . . 10
143142compleqd 3245 . . . . . . . . 9
144143eleq2d 2420 . . . . . . . 8
145 rexeq 2808 . . . . . . . . . 10
146145abbidv 2467 . . . . . . . . 9
147146eleq1d 2419 . . . . . . . 8
148144, 147imbi12d 311 . . . . . . 7
149148rspccv 2952 . . . . . 6
150141, 149syl 15 . . . . 5 Nn
151150com3r 73 . . . 4 Nn
1528, 151vtoclga 2920 . . 3 Nn
153152com3l 75 . 2 Nn
1541533imp 1145 1 Nn
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358   w3a 934  wal 1540   wceq 1642   wcel 1710  cab 2339  wral 2614  wrex 2615   ∼ ccompl 3205   cun 3207   cin 3208  c0 3550  csn 3737  cuni 3891  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   cplc 4375
This theorem is referenced by:  nnadjoinpw  4521
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-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-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  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-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-0c 4377  df-addc 4378  df-nnc 4379
  Copyright terms: Public domain W3C validator