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

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710   ≠ wne 2517  ∃wrex 2616  Vcvv 2860   ∪ cun 3208   ∩ cin 3209   ⊆ wss 3258  ∅c0 3551  {csn 3738  ℘₁cpw1 4136  0_cc0c 4375   +_c cplc 4376   class class class wbr 4640   × 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