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

Theorem pwadjoin 4119
Description: Compute the power class of an adjoinment. (Contributed by SF, 30-Jan-2015.)
Assertion
Ref Expression
pwadjoin
Distinct variable groups:   ,,   ,,

Proof of Theorem pwadjoin
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uncom 3408 . . . . . . . . . . . . . . 15
21sseq2i 3296 . . . . . . . . . . . . . 14
3 ssundif 3633 . . . . . . . . . . . . . 14
42, 3bitri 240 . . . . . . . . . . . . 13
54biimpi 186 . . . . . . . . . . . 12
65adantr 451 . . . . . . . . . . 11
7 vex 2862 . . . . . . . . . . . . 13
8 snex 4111 . . . . . . . . . . . . 13
97, 8difex 4107 . . . . . . . . . . . 12
109elpw 3728 . . . . . . . . . . 11
116, 10sylibr 203 . . . . . . . . . 10
12 difsnid 3854 . . . . . . . . . . . 12
1312eqcomd 2358 . . . . . . . . . . 11
1413adantl 452 . . . . . . . . . 10
15 uneq1 3411 . . . . . . . . . . . 12
1615eqeq2d 2364 . . . . . . . . . . 11
1716rspcev 2955 . . . . . . . . . 10
1811, 14, 17syl2anc 642 . . . . . . . . 9
1918ex 423 . . . . . . . 8
2019con3d 125 . . . . . . 7
21 ssel 3267 . . . . . . . . . . . . 13
2221com12 27 . . . . . . . . . . . 12
23 elun 3220 . . . . . . . . . . . . . . . 16
24 elsn 3748 . . . . . . . . . . . . . . . . 17
2524orbi2i 505 . . . . . . . . . . . . . . . 16
2623, 25bitri 240 . . . . . . . . . . . . . . 15
27 ax-1 6 . . . . . . . . . . . . . . . 16
28 eleq1 2413 . . . . . . . . . . . . . . . . . 18
2928anbi1d 685 . . . . . . . . . . . . . . . . 17
30 pm2.21 100 . . . . . . . . . . . . . . . . . 18
3130impcom 419 . . . . . . . . . . . . . . . . 17
3229, 31syl6bi 219 . . . . . . . . . . . . . . . 16
3327, 32jaoi 368 . . . . . . . . . . . . . . 15
3426, 33sylbi 187 . . . . . . . . . . . . . 14
3534exp3a 425 . . . . . . . . . . . . 13
3635com12 27 . . . . . . . . . . . 12
3722, 36syld 40 . . . . . . . . . . 11
3837imp3a 420 . . . . . . . . . 10
3938com12 27 . . . . . . . . 9
4039ssrdv 3278 . . . . . . . 8
4140ex 423 . . . . . . 7
4220, 41syld 40 . . . . . 6
4342orrd 367 . . . . 5
4443orcomd 377 . . . 4
45 ssun3 3428 . . . . 5
46 vex 2862 . . . . . . . . 9
4746elpw 3728 . . . . . . . 8
48 unss1 3432 . . . . . . . 8
4947, 48sylbi 187 . . . . . . 7
50 sseq1 3292 . . . . . . 7
5149, 50syl5ibrcom 213 . . . . . 6
5251rexlimiv 2732 . . . . 5
5345, 52jaoi 368 . . . 4
5444, 53impbii 180 . . 3
557elpw 3728 . . 3
56 elun 3220 . . . 4
577elpw 3728 . . . . 5
58 eqeq1 2359 . . . . . . 7
5958rexbidv 2635 . . . . . 6
607, 59elab 2985 . . . . 5
6157, 60orbi12i 507 . . . 4
6256, 61bitri 240 . . 3
6354, 55, 623bitr4i 268 . 2
6463eqriv 2350 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wo 357   wa 358   wceq 1642   wcel 1710  cab 2339  wrex 2615   cdif 3206   cun 3207   wss 3257  cpw 3722  csn 3737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  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-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-pw 3724  df-sn 3741
This theorem is referenced by:  nnadjoinpw  4521
  Copyright terms: Public domain W3C validator