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

Theorem phiall 4618
 Description: Any set is equal to either the Phi of another set or to a Phi with 0c adjoined. (Contributed by Scott Fenton, 8-Apr-2021.)
Hypothesis
Ref Expression
phiall.1 A V
Assertion
Ref Expression
phiall x(A = Phi x A = ( Phi x ∪ {0c}))
Distinct variable group:   x,A

Proof of Theorem phiall
StepHypRef Expression
1 neldifsn 3841 . . . . 5 ¬ 0c (A {0c})
2 phiall.1 . . . . . . 7 A V
3 snex 4111 . . . . . . 7 {0c} V
42, 3difex 4107 . . . . . 6 (A {0c}) V
54phialllem2 4617 . . . . 5 (¬ 0c (A {0c}) → x(A {0c}) = Phi x)
61, 5ax-mp 5 . . . 4 x(A {0c}) = Phi x
7 disjsn 3786 . . . . . . . . . 10 (((A {0c}) ∩ {0c}) = ↔ ¬ 0c (A {0c}))
81, 7mpbir 200 . . . . . . . . 9 ((A {0c}) ∩ {0c}) =
9 0cnelphi 4597 . . . . . . . . . 10 ¬ 0c Phi x
10 disjsn 3786 . . . . . . . . . 10 (( Phi x ∩ {0c}) = ↔ ¬ 0c Phi x)
119, 10mpbir 200 . . . . . . . . 9 ( Phi x ∩ {0c}) =
128, 11eqtr4i 2376 . . . . . . . 8 ((A {0c}) ∩ {0c}) = ( Phi x ∩ {0c})
1312biantru 491 . . . . . . 7 (((A {0c}) ∪ {0c}) = ( Phi x ∪ {0c}) ↔ (((A {0c}) ∪ {0c}) = ( Phi x ∪ {0c}) ((A {0c}) ∩ {0c}) = ( Phi x ∩ {0c})))
14 unineq 3505 . . . . . . 7 ((((A {0c}) ∪ {0c}) = ( Phi x ∪ {0c}) ((A {0c}) ∩ {0c}) = ( Phi x ∩ {0c})) ↔ (A {0c}) = Phi x)
1513, 14bitri 240 . . . . . 6 (((A {0c}) ∪ {0c}) = ( Phi x ∪ {0c}) ↔ (A {0c}) = Phi x)
16 difsnid 3854 . . . . . . 7 (0c A → ((A {0c}) ∪ {0c}) = A)
1716eqeq1d 2361 . . . . . 6 (0c A → (((A {0c}) ∪ {0c}) = ( Phi x ∪ {0c}) ↔ A = ( Phi x ∪ {0c})))
1815, 17syl5bbr 250 . . . . 5 (0c A → ((A {0c}) = Phi xA = ( Phi x ∪ {0c})))
1918exbidv 1626 . . . 4 (0c A → (x(A {0c}) = Phi xx A = ( Phi x ∪ {0c})))
206, 19mpbii 202 . . 3 (0c Ax A = ( Phi x ∪ {0c}))
21 olc 373 . . . 4 (A = ( Phi x ∪ {0c}) → (A = Phi x A = ( Phi x ∪ {0c})))
2221eximi 1576 . . 3 (x A = ( Phi x ∪ {0c}) → x(A = Phi x A = ( Phi x ∪ {0c})))
2320, 22syl 15 . 2 (0c Ax(A = Phi x A = ( Phi x ∪ {0c})))
242phialllem2 4617 . . 3 (¬ 0c Ax A = Phi x)
25 orc 374 . . . 4 (A = Phi x → (A = Phi x A = ( Phi x ∪ {0c})))
2625eximi 1576 . . 3 (x A = Phi xx(A = Phi x A = ( Phi x ∪ {0c})))
2724, 26syl 15 . 2 (¬ 0c Ax(A = Phi x A = ( Phi x ∪ {0c})))
2823, 27pm2.61i 156 1 x(A = Phi x A = ( Phi x ∪ {0c}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∨ wo 357   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859   ∖ cdif 3206   ∪ cun 3207   ∩ cin 3208  ∅c0 3550  {csn 3737  0cc0c 4374   Phi cphi 4562 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-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-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-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-0c 4377  df-addc 4378  df-nnc 4379  df-phi 4565 This theorem is referenced by:  opeq  4619
 Copyright terms: Public domain W3C validator