Theorem ce0addcnnul 6179

Description: The sum of two cardinals raised to 0_c is non-empty iff each addend raised to 0_c is non-empty. 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 6144	. . . 4 |- ((M e. NC /\ N e. NC ) -> (M +o N) e. NC )
2		ce0nnul 6177	. . . . 5 |- ((M +o N) e. NC -> (((M +o N) ↑c 0c) =/= (/) <-> E.a~P1 a e. (M +o N)))
3		eladdc 4398	. . . . . 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 6128	. . . . . . . 8 |- (M e. NC -> (M = Nc b <-> b e. M))
8		ncseqnc 6128	. . . . . . . 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 3426	. . . . . . . . . . . 12 |- b C_ (b u. g)
12		id 19	. . . . . . . . . . . 12 |- (~P1 a = (b u. g) -> ~P1 a = (b u. g))
13	11, 12	syl5sseqr 3320	. . . . . . . . . . 11 |- (~P1 a = (b u. g) -> b C_ ~P1 a)
14		ssun2 3427	. . . . . . . . . . . 12 |- g C_ (b u. g)
15	14, 12	syl5sseqr 3320	. . . . . . . . . . 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 2862	. . . . . . . . . . . . 13 |- b e. _V
18	17	sspw1 4335	. . . . . . . . . . . 12 |- (b C_ ~P1 a <-> E.p(p C_ a /\ b = ~P1 p))
19		vex 2862	. . . . . . . . . . . . 13 |- g e. _V
20	19	sspw1 4335	. . . . . . . . . . . 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 4143	. . . . . . . . . . . . . . . . 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 2862	. . . . . . . . . . . . . . . . . 18 |- p e. _V
28	27	pw1ex 4303	. . . . . . . . . . . . . . . . 17 |- ~P1 p e. _V
29	28	ncid 6123	. . . . . . . . . . . . . . . 16 |- ~P1 p e. Nc ~P1 p
30	26, 29	speiv 2000	. . . . . . . . . . . . . . 15 |- E.a~P1 a e. Nc ~P1 p
31		ncelncs 6120	. . . . . . . . . . . . . . . 16 |- (~P1 p e. _V -> Nc ~P1 p e. NC )
32		ce0nnul 6177	. . . . . . . . . . . . . . . 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 4143	. . . . . . . . . . . . . . . . 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 2862	. . . . . . . . . . . . . . . . . 18 |- q e. _V
38	37	pw1ex 4303	. . . . . . . . . . . . . . . . 17 |- ~P1 q e. _V
39	38	ncid 6123	. . . . . . . . . . . . . . . 16 |- ~P1 q e. Nc ~P1 q
40	36, 39	speiv 2000	. . . . . . . . . . . . . . 15 |- E.a~P1 a e. Nc ~P1 q
41		ncelncs 6120	. . . . . . . . . . . . . . . 16 |- (~P1 q e. _V -> Nc ~P1 q e. NC )
42		ce0nnul 6177	. . . . . . . . . . . . . . . 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 6108	. . . . . . . . . . . . . . . 16 |- (b = ~P1 p -> Nc b = Nc ~P1 p)
47	46	oveq1d 5537	. . . . . . . . . . . . . . 15 |- (b = ~P1 p -> ( Nc b ↑c 0c) = ( Nc ~P1 p ↑c 0c))
48	47	neeq1d 2529	. . . . . . . . . . . . . 14 |- (b = ~P1 p -> (( Nc b ↑c 0c) =/= (/) <-> ( Nc ~P1 p ↑c 0c) =/= (/)))
49		nceq 6108	. . . . . . . . . . . . . . . 16 |- (g = ~P1 q -> Nc g = Nc ~P1 q)
50	49	oveq1d 5537	. . . . . . . . . . . . . . 15 |- (g = ~P1 q -> ( Nc g ↑c 0c) = ( Nc ~P1 q ↑c 0c))
51	50	neeq1d 2529	. . . . . . . . . . . . . 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 5530	. . . . . . . . 9 |- (M = Nc b -> (M ↑c 0c) = ( Nc b ↑c 0c))
60	59	neeq1d 2529	. . . . . . . 8 |- (M = Nc b -> ((M ↑c 0c) =/= (/) <-> ( Nc b ↑c 0c) =/= (/)))
61		oveq1 5530	. . . . . . . . 9 |- (N = Nc g -> (N ↑c 0c) = ( Nc g ↑c 0c))
62	61	neeq1d 2529	. . . . . . . 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 2745	. . . 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 6177	. . . . 5 |- (M e. NC -> ((M ↑c 0c) =/= (/) <-> E.b~P1 b e. M))
70		ce0nnul 6177	. . . . 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 6128	. . . . . 6 |- (M e. NC -> (M = Nc ~P1 b <-> ~P1 b e. M))
75		ncseqnc 6128	. . . . . 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 4109	. . . . . . . . . . . 12 |- _V e. _V
78	17, 77	xpsnen 6049	. . . . . . . . . . 11 |- (b X. {_V}) ~~ b
79		enpw1 6062	. . . . . . . . . . 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 4111	. . . . . . . . . . . . 13 |- {_V} e. _V
82	17, 81	xpex 5115	. . . . . . . . . . . 12 |- (b X. {_V}) e. _V
83	82	pw1ex 4303	. . . . . . . . . . 11 |- ~P1 (b X. {_V}) e. _V
84	83	eqnc 6127	. . . . . . . . . 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 4110	. . . . . . . . . . . 12 |- (/) e. _V
87	19, 86	xpsnen 6049	. . . . . . . . . . 11 |- (g X. {(/)}) ~~ g
88		enpw1 6062	. . . . . . . . . . 11 |- ((g X. {(/)}) ~~ g <-> ~P1 (g X. {(/)}) ~~ ~P1 g)
89	87, 88	mpbi 199	. . . . . . . . . 10 |- ~P1 (g X. {(/)}) ~~ ~P1 g
90		snex 4111	. . . . . . . . . . . . 13 |- {(/)} e. _V
91	19, 90	xpex 5115	. . . . . . . . . . . 12 |- (g X. {(/)}) e. _V
92	91	pw1ex 4303	. . . . . . . . . . 11 |- ~P1 (g X. {(/)}) e. _V
93	92	eqnc 6127	. . . . . . . . . 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 4388	. . . . . . . 8 |- ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) = ( Nc ~P1 b +o Nc ~P1 g)
96	95	oveq1i 5533	. . . . . . 7 |- (( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)})) ↑c 0c) = (( Nc ~P1 b +o Nc ~P1 g) ↑c 0c)
97		pw1un 4163	. . . . . . . . . 10 |- ~P1 ((b X. {_V}) u. (g X. {(/)})) = (~P1 (b X. {_V}) u. ~P1 (g X. {(/)}))
98	83	ncid 6123	. . . . . . . . . . 11 |- ~P1 (b X. {_V}) e. Nc ~P1 (b X. {_V})
99	92	ncid 6123	. . . . . . . . . . 11 |- ~P1 (g X. {(/)}) e. Nc ~P1 (g X. {(/)})
100		vn0 3557	. . . . . . . . . . . . . 14 |- _V =/= (/)
101	77, 100	xpnedisj 5513	. . . . . . . . . . . . 13 |- ((b X. {_V}) i^i (g X. {(/)})) = (/)
102		pw1eq 4143	. . . . . . . . . . . . 13 |- (((b X. {_V}) i^i (g X. {(/)})) = (/) -> ~P1 ((b X. {_V}) i^i (g X. {(/)})) = ~P1 (/))
103	101, 102	ax-mp 8	. . . . . . . . . . . 12 |- ~P1 ((b X. {_V}) i^i (g X. {(/)})) = ~P1 (/)
104		pw1in 4164	. . . . . . . . . . . 12 |- ~P1 ((b X. {_V}) i^i (g X. {(/)})) = (~P1 (b X. {_V}) i^i ~P1 (g X. {(/)}))
105		pw10 4161	. . . . . . . . . . . 12 |- ~P1 (/) = (/)
106	103, 104, 105	3eqtr3i 2381	. . . . . . . . . . 11 |- (~P1 (b X. {_V}) i^i ~P1 (g X. {(/)})) = (/)
107		eladdci 4399	. . . . . . . . . . 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 4106	. . . . . . . . . 10 |- ((b X. {_V}) u. (g X. {(/)})) e. _V
111		pw1eq 4143	. . . . . . . . . . 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 2946	. . . . . . . . 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 8	. . . . . . . 8 |- E.a~P1 a e. ( Nc ~P1 (b X. {_V}) +o Nc ~P1 (g X. {(/)}))
115	83	ncelncsi 6121	. . . . . . . . . 10 |- Nc ~P1 (b X. {_V}) e. NC
116	92	ncelncsi 6121	. . . . . . . . . 10 |- Nc ~P1 (g X. {(/)}) e. NC
117		ncaddccl 6144	. . . . . . . . . 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 6177	. . . . . . . . 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 8	. . . . . . . 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 2535	. . . . . 6 |- (( Nc ~P1 b +o Nc ~P1 g) ↑c 0c) =/= (/)
123		addceq12 4385	. . . . . . . 8 |- ((M = Nc ~P1 b /\ N = Nc ~P1 g) -> (M +o N) = ( Nc ~P1 b +o Nc ~P1 g))
124	123	oveq1d 5537	. . . . . . 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 2529	. . . . . 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 2516  E.wrex 2615  _Vcvv 2859   u. cun 3207   i^i cin 3208   C_ wss 3257  (/)c0 3550  {csn 3737  ~P₁ cpw1 4135  0_cc0c 4374   +o cplc 4375   class class class wbr 4639   X. cxp 4770  (class class class)co 5525   ~~ cen 6028   NC cncs 6088   Nc cnc 6091   ↑_c cce 6096

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 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-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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  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-pss 3261  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-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-fv 4795  df-2nd 4797  df-ov 5526  df-oprab 5528  df-mpt 5652  df-mpt2 5654  df-txp 5736  df-ins2 5750  df-ins3 5752  df-image 5754  df-ins4 5756  df-si3 5758  df-funs 5760  df-fns 5762  df-pw1fn 5766  df-trans 5899  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-map 6001  df-en 6029  df-ncs 6098  df-nc 6101  df-ce 6106

This theorem is referenced by:  ce0nn  6180