Theorem ce0addcnnul 6180

Description: The sum of two cardinals raised to 0_c is nonempty iff each addend raised to 0_c is nonempty. Theorem XI.2.43 of [Rosser] p. 383. (Contributed by SF, 9-Mar-2015.)

Assertion

Ref	Expression
ce0addcnnul	|- ((M e. NC /\ N e. NC ) -> (((M +o N) ↑c 0c) =/= (/) <-> ((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/))))

Proof of Theorem ce0addcnnul

Dummy variables a b g p q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ncaddccl 6145	. . . 4 |- ((M e. NC /\ N e. NC ) -> (M +o N) e. NC )
2		ce0nnul 6178	. . . . 5 |- ((M +o N) e. NC -> (((M +o N) ↑c 0c) =/= (/) <-> E.a~P1 a e. (M +o N)))
3		eladdc 4399	. . . . . 6 |- (~P1 a e. (M +o N) <-> E.b e. M E.g e. N ((b i^i g) = (/) /\ ~P1 a = (b u. g)))
4	3	exbii 1582	. . . . 5 |- (E.a~P1 a e. (M +o N) <-> E.aE.b e. M E.g e. N ((b i^i g) = (/) /\ ~P1 a = (b u. g)))
5	2, 4	syl6bb 252	. . . 4 |- ((M +o N) e. NC -> (((M +o N) ↑c 0c) =/= (/) <-> E.aE.b e. M E.g e. N ((b i^i g) = (/) /\ ~P1 a = (b u. g))))
6	1, 5	syl 15	. . 3 |- ((M e. NC /\ N e. NC ) -> (((M +o N) ↑c 0c) =/= (/) <-> E.aE.b e. M E.g e. N ((b i^i g) = (/) /\ ~P1 a = (b u. g))))
7		ncseqnc 6129	. . . . . . . 8 |- (M e. NC -> (M = Nc b <-> b e. M))
8		ncseqnc 6129	. . . . . . . 8 |- (N e. NC -> (N = Nc g <-> g e. N))
9	7, 8	bi2anan9 843	. . . . . . 7 |- ((M e. NC /\ N e. NC ) -> ((M = Nc b /\ N = Nc g) <-> (b e. M /\ g e. N)))
10	9	biimpar 471	. . . . . 6 |- (((M e. NC /\ N e. NC ) /\ (b e. M /\ g e. N)) -> (M = Nc b /\ N = Nc g))
11		ssun1 3427	. . . . . . . . . . . 12 |- b C_ (b u. g)
12		id 19	. . . . . . . . . . . 12 |- (~P1 a = (b u. g) -> ~P1 a = (b u. g))
13	11, 12	syl5sseqr 3321	. . . . . . . . . . 11 |- (~P1 a = (b u. g) -> b C_ ~P1 a)
14		ssun2 3428	. . . . . . . . . . . 12 |- g C_ (b u. g)
15	14, 12	syl5sseqr 3321	. . . . . . . . . . 11 |- (~P1 a = (b u. g) -> g C_ ~P1 a)
16	13, 15	jca 518	. . . . . . . . . 10 |- (~P1 a = (b u. g) -> (b C_ ~P1 a /\ g C_ ~P1 a))
17		vex 2863	. . . . . . . . . . . . 13 |- b e. _V
18	17	sspw1 4336	. . . . . . . . . . . 12 |- (b C_ ~P1 a <-> E.p(p C_ a /\ b = ~P1 p))
19		vex 2863	. . . . . . . . . . . . 13 |- g e. _V
20	19	sspw1 4336	. . . . . . . . . . . 12 |- (g C_ ~P1 a <-> E.q(q C_ a /\ g = ~P1 q))
21	18, 20	anbi12i 678	. . . . . . . . . . 11 |- ((b C_ ~P1 a /\ g C_ ~P1 a) <-> (E.p(p C_ a /\ b = ~P1 p) /\ E.q(q C_ a /\ g = ~P1 q)))
22		eeanv 1913	. . . . . . . . . . 11 |- (E.pE.q((p C_ a /\ b = ~P1 p) /\ (q C_ a /\ g = ~P1 q)) <-> (E.p(p C_ a /\ b = ~P1 p) /\ E.q(q C_ a /\ g = ~P1 q)))
23	21, 22	bitr4i 243	. . . . . . . . . 10 |- ((b C_ ~P1 a /\ g C_ ~P1 a) <-> E.pE.q((p C_ a /\ b = ~P1 p) /\ (q C_ a /\ g = ~P1 q)))
24	16, 23	sylib 188	. . . . . . . . 9 |- (~P1 a = (b u. g) -> E.pE.q((p C_ a /\ b = ~P1 p) /\ (q C_ a /\ g = ~P1 q)))
25		pw1eq 4144	. . . . . . . . . . . . . . . . 17 |- (a = p -> ~P1 a = ~P1 p)
26	25	eleq1d 2419	. . . . . . . . . . . . . . . 16 |- (a = p -> (~P1 a e. Nc ~P1 p <-> ~P1 p e. Nc ~P1 p))
27		vex 2863	. . . . . . . . . . . . . . . . . 18 |- p e. _V
28	27	pw1ex 4304	. . . . . . . . . . . . . . . . 17 |- ~P1 p e. _V
29	28	ncid 6124	. . . . . . . . . . . . . . . 16 |- ~P1 p e. Nc ~P1 p
30	26, 29	speiv 2000	. . . . . . . . . . . . . . 15 |- E.a~P1 a e. Nc ~P1 p
31		ncelncs 6121	. . . . . . . . . . . . . . . 16 |- (~P1 p e. _V -> Nc ~P1 p e. NC )
32		ce0nnul 6178	. . . . . . . . . . . . . . . 16 |- ( Nc ~P1 p e. NC -> (( Nc ~P1 p ↑c 0c) =/= (/) <-> E.a~P1 a e. Nc ~P1 p))
33	28, 31, 32	mp2b 9	. . . . . . . . . . . . . . 15 |- (( Nc ~P1 p ↑c 0c) =/= (/) <-> E.a~P1 a e. Nc ~P1 p)
34	30, 33	mpbir 200	. . . . . . . . . . . . . 14 |- ( Nc ~P1 p ↑c 0c) =/= (/)
35		pw1eq 4144	. . . . . . . . . . . . . . . . 17 |- (a = q -> ~P1 a = ~P1 q)
36	35	eleq1d 2419	. . . . . . . . . . . . . . . 16 |- (a = q -> (~P1 a e. Nc ~P1 q <-> ~P1 q e. Nc ~P1 q))
37		vex 2863	. . . . . . . . . . . . . . . . . 18 |- q e. _V
38	37	pw1ex 4304	. . . . . . . . . . . . . . . . 17 |- ~P1 q e. _V
39	38	ncid 6124	. . . . . . . . . . . . . . . 16 |- ~P1 q e. Nc ~P1 q
40	36, 39	speiv 2000	. . . . . . . . . . . . . . 15 |- E.a~P1 a e. Nc ~P1 q
41		ncelncs 6121	. . . . . . . . . . . . . . . 16 |- (~P1 q e. _V -> Nc ~P1 q e. NC )
42		ce0nnul 6178	. . . . . . . . . . . . . . . 16 |- ( Nc ~P1 q e. NC -> (( Nc ~P1 q ↑c 0c) =/= (/) <-> E.a~P1 a e. Nc ~P1 q))
43	38, 41, 42	mp2b 9	. . . . . . . . . . . . . . 15 |- (( Nc ~P1 q ↑c 0c) =/= (/) <-> E.a~P1 a e. Nc ~P1 q)
44	40, 43	mpbir 200	. . . . . . . . . . . . . 14 |- ( Nc ~P1 q ↑c 0c) =/= (/)
45	34, 44	pm3.2i 441	. . . . . . . . . . . . 13 |- (( Nc ~P1 p ↑c 0c) =/= (/) /\ ( Nc ~P1 q ↑c 0c) =/= (/))
46		nceq 6109	. . . . . . . . . . . . . . . 16 |- (b = ~P1 p -> Nc b = Nc ~P1 p)
47	46	oveq1d 5538	. . . . . . . . . . . . . . 15 |- (b = ~P1 p -> ( Nc b ↑c 0c) = ( Nc ~P1 p ↑c 0c))
48	47	neeq1d 2530	. . . . . . . . . . . . . 14 |- (b = ~P1 p -> (( Nc b ↑c 0c) =/= (/) <-> ( Nc ~P1 p ↑c 0c) =/= (/)))
49		nceq 6109	. . . . . . . . . . . . . . . 16 |- (g = ~P1 q -> Nc g = Nc ~P1 q)
50	49	oveq1d 5538	. . . . . . . . . . . . . . 15 |- (g = ~P1 q -> ( Nc g ↑c 0c) = ( Nc ~P1 q ↑c 0c))
51	50	neeq1d 2530	. . . . . . . . . . . . . 14 |- (g = ~P1 q -> (( Nc g ↑c 0c) =/= (/) <-> ( Nc ~P1 q ↑c 0c) =/= (/)))
52	48, 51	bi2anan9 843	. . . . . . . . . . . . 13 |- ((b = ~P1 p /\ g = ~P1 q) -> ((( Nc b ↑c 0c) =/= (/) /\ ( Nc g ↑c 0c) =/= (/)) <-> (( Nc ~P1 p ↑c 0c) =/= (/) /\ ( Nc ~P1 q ↑c 0c) =/= (/))))
53	45, 52	mpbiri 224	. . . . . . . . . . . 12 |- ((b = ~P1 p /\ g = ~P1 q) -> (( Nc b ↑c 0c) =/= (/) /\ ( Nc g ↑c 0c) =/= (/)))
54	53	ad2ant2l 726	. . . . . . . . . . 11 |- (((p C_ a /\ b = ~P1 p) /\ (q C_ a /\ g = ~P1 q)) -> (( Nc b ↑c 0c) =/= (/) /\ ( Nc g ↑c 0c) =/= (/)))
55	54	a1d 22	. . . . . . . . . 10 |- (((p C_ a /\ b = ~P1 p) /\ (q C_ a /\ g = ~P1 q)) -> ((b i^i g) = (/) -> (( Nc b ↑c 0c) =/= (/) /\ ( Nc g ↑c 0c) =/= (/))))
56	55	exlimivv 1635	. . . . . . . . 9 |- (E.pE.q((p C_ a /\ b = ~P1 p) /\ (q C_ a /\ g = ~P1 q)) -> ((b i^i g) = (/) -> (( Nc b ↑c 0c) =/= (/) /\ ( Nc g ↑c 0c) =/= (/))))
57	24, 56	syl 15	. . . . . . . 8 |- (~P1 a = (b u. g) -> ((b i^i g) = (/) -> (( Nc b ↑c 0c) =/= (/) /\ ( Nc g ↑c 0c) =/= (/))))
58	57	impcom 419	. . . . . . 7 |- (((b i^i g) = (/) /\ ~P1 a = (b u. g)) -> (( Nc b ↑c 0c) =/= (/) /\ ( Nc g ↑c 0c) =/= (/)))
59		oveq1 5531	. . . . . . . . 9 |- (M = Nc b -> (M ↑c 0c) = ( Nc b ↑c 0c))
60	59	neeq1d 2530	. . . . . . . 8 |- (M = Nc b -> ((M ↑c 0c) =/= (/) <-> ( Nc b ↑c 0c) =/= (/)))
61		oveq1 5531	. . . . . . . . 9 |- (N = Nc g -> (N ↑c 0c) = ( Nc g ↑c 0c))
62	61	neeq1d 2530	. . . . . . . 8 |- (N = Nc g -> ((N ↑c 0c) =/= (/) <-> ( Nc g ↑c 0c) =/= (/)))
63	60, 62	bi2anan9 843	. . . . . . 7 |- ((M = Nc b /\ N = Nc g) -> (((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/)) <-> (( Nc b ↑c 0c) =/= (/) /\ ( Nc g ↑c 0c) =/= (/))))
64	58, 63	syl5ibr 212	. . . . . 6 |- ((M = Nc b /\ N = Nc g) -> (((b i^i g) = (/) /\ ~P1 a = (b u. g)) -> ((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/))))
65	10, 64	syl 15	. . . . 5 |- (((M e. NC /\ N e. NC ) /\ (b e. M /\ g e. N)) -> (((b i^i g) = (/) /\ ~P1 a = (b u. g)) -> ((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/))))
66	65	rexlimdvva 2746	. . . 4 |- ((M e. NC /\ N e. NC ) -> (E.b e. M E.g e. N ((b i^i g) = (/) /\ ~P1 a = (b u. g)) -> ((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/))))
67	66	exlimdv 1636	. . 3 |- ((M e. NC /\ N e. NC ) -> (E.aE.b e. M E.g e. N ((b i^i g) = (/) /\ ~P1 a = (b u. g)) -> ((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/))))
68	6, 67	sylbid 206	. 2 |- ((M e. NC /\ N e. NC ) -> (((M +o N) ↑c 0c) =/= (/) -> ((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/))))
69		ce0nnul 6178	. . . . 5 |- (M e. NC -> ((M ↑c 0c) =/= (/) <-> E.b~P1 b e. M))
70		ce0nnul 6178	. . . . 5 |- (N e. NC -> ((N ↑c 0c) =/= (/) <-> E.g~P1 g e. N))
71	69, 70	bi2anan9 843	. . . 4 |- ((M e. NC /\ N e. NC ) -> (((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/)) <-> (E.b~P1 b e. M /\ E.g~P1 g e. N)))
72		eeanv 1913	. . . 4 |- (E.bE.g(~P1 b e. M /\ ~P1 g e. N) <-> (E.b~P1 b e. M /\ E.g~P1 g e. N))
73	71, 72	syl6bbr 254	. . 3 |- ((M e. NC /\ N e. NC ) -> (((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/)) <-> E.bE.g(~P1 b e. M /\ ~P1 g e. N)))
74		ncseqnc 6129	. . . . . 6 |- (M e. NC -> (M = Nc ~P1 b <-> ~P1 b e. M))
75		ncseqnc 6129	. . . . . 6 |- (N e. NC -> (N = Nc ~P1 g <-> ~P1 g e. N))
76	74, 75	bi2anan9 843	. . . . 5 |- ((M e. NC /\ N e. NC ) -> ((M = Nc ~P1 b /\ N = Nc ~P1 g) <-> (~P1 b e. M /\ ~P1 g e. N)))
77		vvex 4110	. . . . . . . . . . . 12 |- _V e. _V
78	17, 77	xpsnen 6050	. . . . . . . . . . 11 |- (b X. {_V}) ~~ b
79		enpw1 6063	. . . . . . . . . . 11 |- ((b X. {_V}) ~~ b <-> ~P1 (b X. {_V}) ~~ ~P1 b)
80	78, 79	mpbi 199	. . . . . . . . . 10 |- ~P1 (b X. {_V}) ~~ ~P1 b
81		snex 4112	. . . . . . . . . . . . 13 |- {_V} e. _V
82	17, 81	xpex 5116	. . . . . . . . . . . 12 |- (b X. {_V}) e. _V
83	82	pw1ex 4304	. . . . . . . . . . 11 |- ~P1 (b X. {_V}) e. _V
84	83	eqnc 6128	. . . . . . . . . 10 |- ( Nc ~P1 (b X. {_V}) = Nc ~P1 b <-> ~P1 (b X. {_V}) ~~ ~P1 b)
85	80, 84	mpbir 200	. . . . . . . . 9 |- Nc ~P1 (b X. {_V}) = Nc ~P1 b
86		0ex 4111	. . . . . . . . . . . 12 |- (/) e. _V
87	19, 86	xpsnen 6050	. . . . . . . . . . 11 |- (g X. {(/)}) ~~ g
88		enpw1 6063	. . . . . . . . . . 11 |- ((g X. {(/)}) ~~ g <-> ~P1 (g X. {(/)}) ~~ ~P1 g)
89	87, 88	mpbi 199	. . . . . . . . . 10 |- ~P1 (g X. {(/)}) ~~ ~P1 g
90		snex 4112	. . . . . . . . . . . . 13 |- {(/)} e. _V
91	19, 90	xpex 5116	. . . . . . . . . . . 12 |- (g X. {(/)}) e. _V
92	91	pw1ex 4304	. . . . . . . . . . 11 |- ~P1 (g X. {(/)}) e. _V
93	92	eqnc 6128	. . . . . . . . . 10 |- ( Nc ~P1 (g X. {(/)}) = Nc ~P1 g <-> ~P1 (g X. {(/)}) ~~ ~P1 g)
94	89, 93	mpbir 200	. . . . . . . . 9 |- Nc ~P1 (g X. {(/)}) = Nc ~P1 g
95	85, 94	addceq12i 4389	. . . . . . . 8 |- ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) = ( Nc ~P1 b +o Nc ~P1 g)
96	95	oveq1i 5534	. . . . . . 7 |- (( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) ↑c 0c) = (( Nc ~P1 b +o Nc ~P1 g) ↑c 0c)
97		pw1un 4164	. . . . . . . . . 10 |- ~P1 ((b X. {_V}) u. (g X. {(/)})) = (~P1 (b X. {_V}) u. ~P1 (g X. {(/)}))
98	83	ncid 6124	. . . . . . . . . . 11 |- ~P1 (b X. {_V}) e. Nc ~P1 (b X. {_V})
99	92	ncid 6124	. . . . . . . . . . 11 |- ~P1 (g X. {(/)}) e. Nc ~P1 (g X. {(/)})
100		vn0 3558	. . . . . . . . . . . . . 14 |- _V =/= (/)
101	77, 100	xpnedisj 5514	. . . . . . . . . . . . 13 |- ((b X. {_V}) i^i (g X. {(/)})) = (/)
102		pw1eq 4144	. . . . . . . . . . . . 13 |- (((b X. {_V}) i^i (g X. {(/)})) = (/) -> ~P1 ((b X. {_V}) i^i (g X. {(/)})) = ~P1 (/))
103	101, 102	ax-mp 5	. . . . . . . . . . . 12 |- ~P1 ((b X. {_V}) i^i (g X. {(/)})) = ~P1 (/)
104		pw1in 4165	. . . . . . . . . . . 12 |- ~P1 ((b X. {_V}) i^i (g X. {(/)})) = (~P1 (b X. {_V}) i^i ~P1 (g X. {(/)}))
105		pw10 4162	. . . . . . . . . . . 12 |- ~P1 (/) = (/)
106	103, 104, 105	3eqtr3i 2381	. . . . . . . . . . 11 |- (~P1 (b X. {_V}) i^i ~P1 (g X. {(/)})) = (/)
107		eladdci 4400	. . . . . . . . . . 11 |- ((~P1 (b X. {_V}) e. Nc ~P1 (b X. {_V}) /\ ~P1 (g X. {(/)}) e. Nc ~P1 (g X. {(/)}) /\ (~P1 (b X. {_V}) i^i ~P1 (g X. {(/)})) = (/)) -> (~P1 (b X. {_V}) u. ~P1 (g X. {(/)})) e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})))
108	98, 99, 106, 107	mp3an 1277	. . . . . . . . . 10 |- (~P1 (b X. {_V}) u. ~P1 (g X. {(/)})) e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)}))
109	97, 108	eqeltri 2423	. . . . . . . . 9 |- ~P1 ((b X. {_V}) u. (g X. {(/)})) e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)}))
110	82, 91	unex 4107	. . . . . . . . . 10 |- ((b X. {_V}) u. (g X. {(/)})) e. _V
111		pw1eq 4144	. . . . . . . . . . 11 |- (a = ((b X. {_V}) u. (g X. {(/)})) -> ~P1 a = ~P1 ((b X. {_V}) u. (g X. {(/)})))
112	111	eleq1d 2419	. . . . . . . . . 10 |- (a = ((b X. {_V}) u. (g X. {(/)})) -> (~P1 a e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) <-> ~P1 ((b X. {_V}) u. (g X. {(/)})) e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)}))))
113	110, 112	spcev 2947	. . . . . . . . 9 |- (~P1 ((b X. {_V}) u. (g X. {(/)})) e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) -> E.a~P1 a e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})))
114	109, 113	ax-mp 5	. . . . . . . 8 |- E.a~P1 a e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)}))
115	83	ncelncsi 6122	. . . . . . . . . 10 |- Nc ~P1 (b X. {_V}) e. NC
116	92	ncelncsi 6122	. . . . . . . . . 10 |- Nc ~P1 (g X. {(/)}) e. NC
117		ncaddccl 6145	. . . . . . . . . 10 |- (( Nc ~P1 (b X. {_V}) e. NC /\ Nc ~P1 (g X. {(/)}) e. NC ) -> ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) e. NC )
118	115, 116, 117	mp2an 653	. . . . . . . . 9 |- ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) e. NC
119		ce0nnul 6178	. . . . . . . . 9 |- (( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) e. NC -> ((( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) ↑c 0c) =/= (/) <-> E.a~P1 a e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)}))))
120	118, 119	ax-mp 5	. . . . . . . 8 |- ((( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) ↑c 0c) =/= (/) <-> E.a~P1 a e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})))
121	114, 120	mpbir 200	. . . . . . 7 |- (( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) ↑c 0c) =/= (/)
122	96, 121	eqnetrri 2536	. . . . . 6 |- (( Nc ~P1 b +o Nc ~P1 g) ↑c 0c) =/= (/)
123		addceq12 4386	. . . . . . . 8 |- ((M = Nc ~P1 b /\ N = Nc ~P1 g) -> (M +o N) = ( Nc ~P1 b +o Nc ~P1 g))
124	123	oveq1d 5538	. . . . . . 7 |- ((M = Nc ~P1 b /\ N = Nc ~P1 g) -> ((M +o N) ↑c 0c) = (( Nc ~P1 b +o Nc ~P1 g) ↑c 0c))
125	124	neeq1d 2530	. . . . . 6 |- ((M = Nc ~P1 b /\ N = Nc ~P1 g) -> (((M +o N) ↑c 0c) =/= (/) <-> (( Nc ~P1 b +o Nc ~P1 g) ↑c 0c) =/= (/)))
126	122, 125	mpbiri 224	. . . . 5 |- ((M = Nc ~P1 b /\ N = Nc ~P1 g) -> ((M +o N) ↑c 0c) =/= (/))
127	76, 126	syl6bir 220	. . . 4 |- ((M e. NC /\ N e. NC ) -> ((~P1 b e. M /\ ~P1 g e. N) -> ((M +o N) ↑c 0c) =/= (/)))
128	127	exlimdvv 1637	. . 3 |- ((M e. NC /\ N e. NC ) -> (E.bE.g(~P1 b e. M /\ ~P1 g e. N) -> ((M +o N) ↑c 0c) =/= (/)))
129	73, 128	sylbid 206	. 2 |- ((M e. NC /\ N e. NC ) -> (((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/)) -> ((M +o N) ↑c 0c) =/= (/)))
130	68, 129	impbid 183	1 |- ((M e. NC /\ N e. NC ) -> (((M +o N) ↑c 0c) =/= (/) <-> ((M ↑c 0c) =/= (/) /\ (N ↑c 0c) =/= (/))))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710   =/= wne 2517  E.wrex 2616  _Vcvv 2860   u. cun 3208   i^i cin 3209   C_ wss 3258  (/)c0 3551  {csn 3738  ~P₁ cpw1 4136  0_cc0c 4375   +o cplc 4376   class class class wbr 4640   X. cxp 4771  (class class class)co 5526   ~~ cen 6029   NC cncs 6089   Nc cnc 6092   ↑_c cce 6097

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-13 1712  ax-14 1714  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-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-swap 4725  df-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-dm 4788  df-res 4789  df-fun 4790  df-fn 4791  df-f 4792  df-f1 4793  df-fo 4794  df-f1o 4795  df-fv 4796  df-2nd 4798  df-ov 5527  df-oprab 5529  df-mpt 5653  df-mpt2 5655  df-txp 5737  df-ins2 5751  df-ins3 5753  df-image 5755  df-ins4 5757  df-si3 5759  df-funs 5761  df-fns 5763  df-pw1fn 5767  df-trans 5900  df-sym 5909  df-er 5910  df-ec 5948  df-qs 5952  df-map 6002  df-en 6030  df-ncs 6099  df-nc 6102  df-ce 6107

This theorem is referenced by:  ce0nn  6181