Theorem pw1eqadj 4333

Description: A condition for a unit power class to work out to an adjunction. (Contributed by SF, 26-Jan-2015.)

Hypotheses

Ref	Expression
pw1eqadj.1	|- A e. _V
pw1eqadj.2	|- B e. _V

Assertion

Ref	Expression
pw1eqadj	|- (~P1 C = (A u. {B}) <-> E.xE.y(C = (x u. {y}) /\ A = ~P1 x /\ B = {y}))

Distinct variable groups:   x,A,y   x,B,y   x,C,y

Proof of Theorem pw1eqadj

Step	Hyp	Ref	Expression
1		unieq 3901	. . . . 5 |- (~P1 C = (A u. {B}) -> U.~P1 C = U.(A u. {B}))
2		unipw1 4326	. . . . 5 |- U.~P1 C = C
3		uniun 3911	. . . . 5 |- U.(A u. {B}) = (U.A u. U.{B})
4	1, 2, 3	3eqtr3g 2408	. . . 4 |- (~P1 C = (A u. {B}) -> C = (U.A u. U.{B}))
5		pw1eqadj.2	. . . . . . 7 |- B e. _V
6	5	unisn 3908	. . . . . 6 |- U.{B} = B
7		pw1ss1c 4159	. . . . . . . 8 |- ~P1 C C_ 1c
8		ssun2 3428	. . . . . . . . . 10 |- {B} C_ (A u. {B})
9	5	snid 3761	. . . . . . . . . 10 |- B e. {B}
10	8, 9	sselii 3271	. . . . . . . . 9 |- B e. (A u. {B})
11		eleq2 2414	. . . . . . . . 9 |- (~P1 C = (A u. {B}) -> (B e. ~P1 C <-> B e. (A u. {B})))
12	10, 11	mpbiri 224	. . . . . . . 8 |- (~P1 C = (A u. {B}) -> B e. ~P1 C)
13	7, 12	sseldi 3272	. . . . . . 7 |- (~P1 C = (A u. {B}) -> B e. 1c)
14		el1c 4140	. . . . . . . 8 |- (B e. 1c <-> E.x B = {x})
15		vex 2863	. . . . . . . . . . . . 13 |- x e. _V
16	15	unisn 3908	. . . . . . . . . . . 12 |- U.{x} = x
17	16	sneqi 3746	. . . . . . . . . . 11 |- {U.{x}} = {x}
18	17	eqcomi 2357	. . . . . . . . . 10 |- {x} = {U.{x}}
19		id 19	. . . . . . . . . 10 |- (B = {x} -> B = {x})
20		unieq 3901	. . . . . . . . . . 11 |- (B = {x} -> U.B = U.{x})
21	20	sneqd 3747	. . . . . . . . . 10 |- (B = {x} -> {U.B} = {U.{x}})
22	18, 19, 21	3eqtr4a 2411	. . . . . . . . 9 |- (B = {x} -> B = {U.B})
23	22	exlimiv 1634	. . . . . . . 8 |- (E.x B = {x} -> B = {U.B})
24	14, 23	sylbi 187	. . . . . . 7 |- (B e. 1c -> B = {U.B})
25	13, 24	syl 15	. . . . . 6 |- (~P1 C = (A u. {B}) -> B = {U.B})
26	6, 25	syl5eq 2397	. . . . 5 |- (~P1 C = (A u. {B}) -> U.{B} = {U.B})
27	26	uneq2d 3419	. . . 4 |- (~P1 C = (A u. {B}) -> (U.A u. U.{B}) = (U.A u. {U.B}))
28	4, 27	eqtrd 2385	. . 3 |- (~P1 C = (A u. {B}) -> C = (U.A u. {U.B}))
29		ssun1 3427	. . . . . 6 |- A C_ (A u. {B})
30		sseq2 3294	. . . . . 6 |- (~P1 C = (A u. {B}) -> (A C_ ~P1 C <-> A C_ (A u. {B})))
31	29, 30	mpbiri 224	. . . . 5 |- (~P1 C = (A u. {B}) -> A C_ ~P1 C)
32	31, 7	syl6ss 3285	. . . 4 |- (~P1 C = (A u. {B}) -> A C_ 1c)
33		eqpw1uni 4331	. . . 4 |- (A C_ 1c -> A = ~P1 U.A)
34	32, 33	syl 15	. . 3 |- (~P1 C = (A u. {B}) -> A = ~P1 U.A)
35		pw1eqadj.1	. . . . 5 |- A e. _V
36	35	uniex 4318	. . . 4 |- U.A e. _V
37	5	uniex 4318	. . . 4 |- U.B e. _V
38		sneq 3745	. . . . . . 7 |- (y = U.B -> {y} = {U.B})
39		uneq12 3414	. . . . . . 7 |- ((x = U.A /\ {y} = {U.B}) -> (x u. {y}) = (U.A u. {U.B}))
40	38, 39	sylan2 460	. . . . . 6 |- ((x = U.A /\ y = U.B) -> (x u. {y}) = (U.A u. {U.B}))
41	40	eqeq2d 2364	. . . . 5 |- ((x = U.A /\ y = U.B) -> (C = (x u. {y}) <-> C = (U.A u. {U.B})))
42		pw1eq 4144	. . . . . . 7 |- (x = U.A -> ~P1 x = ~P1 U.A)
43	42	eqeq2d 2364	. . . . . 6 |- (x = U.A -> (A = ~P1 x <-> A = ~P1 U.A))
44	43	adantr 451	. . . . 5 |- ((x = U.A /\ y = U.B) -> (A = ~P1 x <-> A = ~P1 U.A))
45	38	eqeq2d 2364	. . . . . 6 |- (y = U.B -> (B = {y} <-> B = {U.B}))
46	45	adantl 452	. . . . 5 |- ((x = U.A /\ y = U.B) -> (B = {y} <-> B = {U.B}))
47	41, 44, 46	3anbi123d 1252	. . . 4 |- ((x = U.A /\ y = U.B) -> ((C = (x u. {y}) /\ A = ~P1 x /\ B = {y}) <-> (C = (U.A u. {U.B}) /\ A = ~P1 U.A /\ B = {U.B})))
48	36, 37, 47	spc2ev 2948	. . 3 |- ((C = (U.A u. {U.B}) /\ A = ~P1 U.A /\ B = {U.B}) -> E.xE.y(C = (x u. {y}) /\ A = ~P1 x /\ B = {y}))
49	28, 34, 25, 48	syl3anc 1182	. 2 |- (~P1 C = (A u. {B}) -> E.xE.y(C = (x u. {y}) /\ A = ~P1 x /\ B = {y}))
50		pw1un 4164	. . . . 5 |- ~P1 (x u. {y}) = (~P1 x u. ~P1 {y})
51		vex 2863	. . . . . . 7 |- y e. _V
52	51	pw1sn 4166	. . . . . 6 |- ~P1 {y} = {{y}}
53	52	uneq2i 3416	. . . . 5 |- (~P1 x u. ~P1 {y}) = (~P1 x u. {{y}})
54	50, 53	eqtri 2373	. . . 4 |- ~P1 (x u. {y}) = (~P1 x u. {{y}})
55		pw1eq 4144	. . . . . 6 |- (C = (x u. {y}) -> ~P1 C = ~P1 (x u. {y}))
56		sneq 3745	. . . . . . 7 |- (B = {y} -> {B} = {{y}})
57		uneq12 3414	. . . . . . 7 |- ((A = ~P1 x /\ {B} = {{y}}) -> (A u. {B}) = (~P1 x u. {{y}}))
58	56, 57	sylan2 460	. . . . . 6 |- ((A = ~P1 x /\ B = {y}) -> (A u. {B}) = (~P1 x u. {{y}}))
59	55, 58	eqeqan12d 2368	. . . . 5 |- ((C = (x u. {y}) /\ (A = ~P1 x /\ B = {y})) -> (~P1 C = (A u. {B}) <-> ~P1 (x u. {y}) = (~P1 x u. {{y}})))
60	59	3impb 1147	. . . 4 |- ((C = (x u. {y}) /\ A = ~P1 x /\ B = {y}) -> (~P1 C = (A u. {B}) <-> ~P1 (x u. {y}) = (~P1 x u. {{y}})))
61	54, 60	mpbiri 224	. . 3 |- ((C = (x u. {y}) /\ A = ~P1 x /\ B = {y}) -> ~P1 C = (A u. {B}))
62	61	exlimivv 1635	. 2 |- (E.xE.y(C = (x u. {y}) /\ A = ~P1 x /\ B = {y}) -> ~P1 C = (A u. {B}))
63	49, 62	impbii 180	1 |- (~P1 C = (A u. {B}) <-> E.xE.y(C = (x u. {y}) /\ A = ~P1 x /\ B = {y}))

Syntax hints:   <-> wb 176   /\ wa 358   /\ w3a 934  E.wex 1541   = wceq 1642   e. wcel 1710  _Vcvv 2860   u. cun 3208   C_ wss 3258  {csn 3738  U.cuni 3892  1_cc1c 4135  ~P₁ cpw1 4136

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 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-typlower 4087  ax-sn 4088

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 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-imak 4190  df-p6 4192  df-sik 4193  df-ssetk 4194

This theorem is referenced by:  ncfinlower  4484  sfindbl  4531