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

Theorem pwadjoin 4119
Description: Compute the power class of an adjoinment. (Contributed by SF, 30-Jan-2015.)
Assertion
Ref Expression
pwadjoin (A ∪ {X}) = (A ∪ {a b Aa = (b ∪ {X})})
Distinct variable groups:   A,a,b   X,a,b

Proof of Theorem pwadjoin
Dummy variables x z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uncom 3408 . . . . . . . . . . . . . . 15 (A ∪ {X}) = ({X} ∪ A)
21sseq2i 3296 . . . . . . . . . . . . . 14 (z (A ∪ {X}) ↔ z ({X} ∪ A))
3 ssundif 3633 . . . . . . . . . . . . . 14 (z ({X} ∪ A) ↔ (z {X}) A)
42, 3bitri 240 . . . . . . . . . . . . 13 (z (A ∪ {X}) ↔ (z {X}) A)
54biimpi 186 . . . . . . . . . . . 12 (z (A ∪ {X}) → (z {X}) A)
65adantr 451 . . . . . . . . . . 11 ((z (A ∪ {X}) X z) → (z {X}) A)
7 vex 2862 . . . . . . . . . . . . 13 z V
8 snex 4111 . . . . . . . . . . . . 13 {X} V
97, 8difex 4107 . . . . . . . . . . . 12 (z {X}) V
109elpw 3728 . . . . . . . . . . 11 ((z {X}) A ↔ (z {X}) A)
116, 10sylibr 203 . . . . . . . . . 10 ((z (A ∪ {X}) X z) → (z {X}) A)
12 difsnid 3854 . . . . . . . . . . . 12 (X z → ((z {X}) ∪ {X}) = z)
1312eqcomd 2358 . . . . . . . . . . 11 (X zz = ((z {X}) ∪ {X}))
1413adantl 452 . . . . . . . . . 10 ((z (A ∪ {X}) X z) → z = ((z {X}) ∪ {X}))
15 uneq1 3411 . . . . . . . . . . . 12 (b = (z {X}) → (b ∪ {X}) = ((z {X}) ∪ {X}))
1615eqeq2d 2364 . . . . . . . . . . 11 (b = (z {X}) → (z = (b ∪ {X}) ↔ z = ((z {X}) ∪ {X})))
1716rspcev 2955 . . . . . . . . . 10 (((z {X}) A z = ((z {X}) ∪ {X})) → b Az = (b ∪ {X}))
1811, 14, 17syl2anc 642 . . . . . . . . 9 ((z (A ∪ {X}) X z) → b Az = (b ∪ {X}))
1918ex 423 . . . . . . . 8 (z (A ∪ {X}) → (X zb Az = (b ∪ {X})))
2019con3d 125 . . . . . . 7 (z (A ∪ {X}) → (¬ b Az = (b ∪ {X}) → ¬ X z))
21 ssel 3267 . . . . . . . . . . . . 13 (z (A ∪ {X}) → (x zx (A ∪ {X})))
2221com12 27 . . . . . . . . . . . 12 (x z → (z (A ∪ {X}) → x (A ∪ {X})))
23 elun 3220 . . . . . . . . . . . . . . . 16 (x (A ∪ {X}) ↔ (x A x {X}))
24 elsn 3748 . . . . . . . . . . . . . . . . 17 (x {X} ↔ x = X)
2524orbi2i 505 . . . . . . . . . . . . . . . 16 ((x A x {X}) ↔ (x A x = X))
2623, 25bitri 240 . . . . . . . . . . . . . . 15 (x (A ∪ {X}) ↔ (x A x = X))
27 ax-1 6 . . . . . . . . . . . . . . . 16 (x A → ((x z ¬ X z) → x A))
28 eleq1 2413 . . . . . . . . . . . . . . . . . 18 (x = X → (x zX z))
2928anbi1d 685 . . . . . . . . . . . . . . . . 17 (x = X → ((x z ¬ X z) ↔ (X z ¬ X z)))
30 pm2.21 100 . . . . . . . . . . . . . . . . . 18 X z → (X zx A))
3130impcom 419 . . . . . . . . . . . . . . . . 17 ((X z ¬ X z) → x A)
3229, 31syl6bi 219 . . . . . . . . . . . . . . . 16 (x = X → ((x z ¬ X z) → x A))
3327, 32jaoi 368 . . . . . . . . . . . . . . 15 ((x A x = X) → ((x z ¬ X z) → x A))
3426, 33sylbi 187 . . . . . . . . . . . . . 14 (x (A ∪ {X}) → ((x z ¬ X z) → x A))
3534exp3a 425 . . . . . . . . . . . . 13 (x (A ∪ {X}) → (x z → (¬ X zx A)))
3635com12 27 . . . . . . . . . . . 12 (x z → (x (A ∪ {X}) → (¬ X zx A)))
3722, 36syld 40 . . . . . . . . . . 11 (x z → (z (A ∪ {X}) → (¬ X zx A)))
3837imp3a 420 . . . . . . . . . 10 (x z → ((z (A ∪ {X}) ¬ X z) → x A))
3938com12 27 . . . . . . . . 9 ((z (A ∪ {X}) ¬ X z) → (x zx A))
4039ssrdv 3278 . . . . . . . 8 ((z (A ∪ {X}) ¬ X z) → z A)
4140ex 423 . . . . . . 7 (z (A ∪ {X}) → (¬ X zz A))
4220, 41syld 40 . . . . . 6 (z (A ∪ {X}) → (¬ b Az = (b ∪ {X}) → z A))
4342orrd 367 . . . . 5 (z (A ∪ {X}) → (b Az = (b ∪ {X}) z A))
4443orcomd 377 . . . 4 (z (A ∪ {X}) → (z A b Az = (b ∪ {X})))
45 ssun3 3428 . . . . 5 (z Az (A ∪ {X}))
46 vex 2862 . . . . . . . . 9 b V
4746elpw 3728 . . . . . . . 8 (b Ab A)
48 unss1 3432 . . . . . . . 8 (b A → (b ∪ {X}) (A ∪ {X}))
4947, 48sylbi 187 . . . . . . 7 (b A → (b ∪ {X}) (A ∪ {X}))
50 sseq1 3292 . . . . . . 7 (z = (b ∪ {X}) → (z (A ∪ {X}) ↔ (b ∪ {X}) (A ∪ {X})))
5149, 50syl5ibrcom 213 . . . . . 6 (b A → (z = (b ∪ {X}) → z (A ∪ {X})))
5251rexlimiv 2732 . . . . 5 (b Az = (b ∪ {X}) → z (A ∪ {X}))
5345, 52jaoi 368 . . . 4 ((z A b Az = (b ∪ {X})) → z (A ∪ {X}))
5444, 53impbii 180 . . 3 (z (A ∪ {X}) ↔ (z A b Az = (b ∪ {X})))
557elpw 3728 . . 3 (z (A ∪ {X}) ↔ z (A ∪ {X}))
56 elun 3220 . . . 4 (z (A ∪ {a b Aa = (b ∪ {X})}) ↔ (z A z {a b Aa = (b ∪ {X})}))
577elpw 3728 . . . . 5 (z Az A)
58 eqeq1 2359 . . . . . . 7 (a = z → (a = (b ∪ {X}) ↔ z = (b ∪ {X})))
5958rexbidv 2635 . . . . . 6 (a = z → (b Aa = (b ∪ {X}) ↔ b Az = (b ∪ {X})))
607, 59elab 2985 . . . . 5 (z {a b Aa = (b ∪ {X})} ↔ b Az = (b ∪ {X}))
6157, 60orbi12i 507 . . . 4 ((z A z {a b Aa = (b ∪ {X})}) ↔ (z A b Az = (b ∪ {X})))
6256, 61bitri 240 . . 3 (z (A ∪ {a b Aa = (b ∪ {X})}) ↔ (z A b Az = (b ∪ {X})))
6354, 55, 623bitr4i 268 . 2 (z (A ∪ {X}) ↔ z (A ∪ {a b Aa = (b ∪ {X})}))
6463eqriv 2350 1 (A ∪ {X}) = (A ∪ {a b Aa = (b ∪ {X})})
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