Theorem ncfinlower 4484

Description: If the unit power classes of two sets are in the same natural, then so are the sets themselves. Theorem X.1.26 of [Rosser] p. 527. (Contributed by SF, 22-Jan-2015.)

Assertion

Ref	Expression
ncfinlower	⊢ ((M ∈ Nn ∧ ℘1A ∈ M ∧ ℘1B ∈ M) → ∃n ∈ Nn (A ∈ n ∧ B ∈ n))

Distinct variable groups:   A,n   B,n

Allowed substitution hint:   M(n)

Proof of Theorem ncfinlower

Dummy variables a b m k c d x y e f w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ncfinlowerlem1 4483	. . . 4 ⊢ {m ∣ ∀a∀b((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))} ∈ V
2		eleq2 2414	. . . . . . 7 ⊢ (m = 0c → (℘1a ∈ m ↔ ℘1a ∈ 0c))
3		eleq2 2414	. . . . . . 7 ⊢ (m = 0c → (℘1b ∈ m ↔ ℘1b ∈ 0c))
4	2, 3	anbi12d 691	. . . . . 6 ⊢ (m = 0c → ((℘1a ∈ m ∧ ℘1b ∈ m) ↔ (℘1a ∈ 0c ∧ ℘1b ∈ 0c)))
5	4	imbi1d 308	. . . . 5 ⊢ (m = 0c → (((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ((℘1a ∈ 0c ∧ ℘1b ∈ 0c) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
6	5	2albidv 1627	. . . 4 ⊢ (m = 0c → (∀a∀b((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ∀a∀b((℘1a ∈ 0c ∧ ℘1b ∈ 0c) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
7		eleq2 2414	. . . . . . 7 ⊢ (m = k → (℘1a ∈ m ↔ ℘1a ∈ k))
8		eleq2 2414	. . . . . . 7 ⊢ (m = k → (℘1b ∈ m ↔ ℘1b ∈ k))
9	7, 8	anbi12d 691	. . . . . 6 ⊢ (m = k → ((℘1a ∈ m ∧ ℘1b ∈ m) ↔ (℘1a ∈ k ∧ ℘1b ∈ k)))
10	9	imbi1d 308	. . . . 5 ⊢ (m = k → (((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
11	10	2albidv 1627	. . . 4 ⊢ (m = k → (∀a∀b((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
12		eleq2 2414	. . . . . . 7 ⊢ (m = (k +c 1c) → (℘1a ∈ m ↔ ℘1a ∈ (k +c 1c)))
13		eleq2 2414	. . . . . . 7 ⊢ (m = (k +c 1c) → (℘1b ∈ m ↔ ℘1b ∈ (k +c 1c)))
14	12, 13	anbi12d 691	. . . . . 6 ⊢ (m = (k +c 1c) → ((℘1a ∈ m ∧ ℘1b ∈ m) ↔ (℘1a ∈ (k +c 1c) ∧ ℘1b ∈ (k +c 1c))))
15	14	imbi1d 308	. . . . 5 ⊢ (m = (k +c 1c) → (((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ((℘1a ∈ (k +c 1c) ∧ ℘1b ∈ (k +c 1c)) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
16	15	2albidv 1627	. . . 4 ⊢ (m = (k +c 1c) → (∀a∀b((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ∀a∀b((℘1a ∈ (k +c 1c) ∧ ℘1b ∈ (k +c 1c)) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
17		eleq2 2414	. . . . . . 7 ⊢ (m = M → (℘1a ∈ m ↔ ℘1a ∈ M))
18		eleq2 2414	. . . . . . 7 ⊢ (m = M → (℘1b ∈ m ↔ ℘1b ∈ M))
19	17, 18	anbi12d 691	. . . . . 6 ⊢ (m = M → ((℘1a ∈ m ∧ ℘1b ∈ m) ↔ (℘1a ∈ M ∧ ℘1b ∈ M)))
20	19	imbi1d 308	. . . . 5 ⊢ (m = M → (((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ((℘1a ∈ M ∧ ℘1b ∈ M) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
21	20	2albidv 1627	. . . 4 ⊢ (m = M → (∀a∀b((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ∀a∀b((℘1a ∈ M ∧ ℘1b ∈ M) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
22		el0c 4422	. . . . . . 7 ⊢ (℘1a ∈ 0c ↔ ℘1a = ∅)
23		pw10b 4167	. . . . . . 7 ⊢ (℘1a = ∅ ↔ a = ∅)
24	22, 23	bitri 240	. . . . . 6 ⊢ (℘1a ∈ 0c ↔ a = ∅)
25		el0c 4422	. . . . . . 7 ⊢ (℘1b ∈ 0c ↔ ℘1b = ∅)
26		pw10b 4167	. . . . . . 7 ⊢ (℘1b = ∅ ↔ b = ∅)
27	25, 26	bitri 240	. . . . . 6 ⊢ (℘1b ∈ 0c ↔ b = ∅)
28		peano1 4403	. . . . . . . 8 ⊢ 0c ∈ Nn
29		nulel0c 4423	. . . . . . . 8 ⊢ ∅ ∈ 0c
30		eleq2 2414	. . . . . . . . 9 ⊢ (n = 0c → (∅ ∈ n ↔ ∅ ∈ 0c))
31	30	rspcev 2956	. . . . . . . 8 ⊢ ((0c ∈ Nn ∧ ∅ ∈ 0c) → ∃n ∈ Nn ∅ ∈ n)
32	28, 29, 31	mp2an 653	. . . . . . 7 ⊢ ∃n ∈ Nn ∅ ∈ n
33		eleq1 2413	. . . . . . . . . 10 ⊢ (a = ∅ → (a ∈ n ↔ ∅ ∈ n))
34		eleq1 2413	. . . . . . . . . 10 ⊢ (b = ∅ → (b ∈ n ↔ ∅ ∈ n))
35	33, 34	bi2anan9 843	. . . . . . . . 9 ⊢ ((a = ∅ ∧ b = ∅) → ((a ∈ n ∧ b ∈ n) ↔ (∅ ∈ n ∧ ∅ ∈ n)))
36		anidm 625	. . . . . . . . 9 ⊢ ((∅ ∈ n ∧ ∅ ∈ n) ↔ ∅ ∈ n)
37	35, 36	syl6bb 252	. . . . . . . 8 ⊢ ((a = ∅ ∧ b = ∅) → ((a ∈ n ∧ b ∈ n) ↔ ∅ ∈ n))
38	37	rexbidv 2636	. . . . . . 7 ⊢ ((a = ∅ ∧ b = ∅) → (∃n ∈ Nn (a ∈ n ∧ b ∈ n) ↔ ∃n ∈ Nn ∅ ∈ n))
39	32, 38	mpbiri 224	. . . . . 6 ⊢ ((a = ∅ ∧ b = ∅) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))
40	24, 27, 39	syl2anb 465	. . . . 5 ⊢ ((℘1a ∈ 0c ∧ ℘1b ∈ 0c) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))
41	40	gen2 1547	. . . 4 ⊢ ∀a∀b((℘1a ∈ 0c ∧ ℘1b ∈ 0c) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))
42		nfv 1619	. . . . . . 7 ⊢ Ⅎa k ∈ Nn
43		nfa1 1788	. . . . . . 7 ⊢ Ⅎa∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))
44	42, 43	nfan 1824	. . . . . 6 ⊢ Ⅎa(k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)))
45		nfv 1619	. . . . . . . 8 ⊢ Ⅎb k ∈ Nn
46		nfa2 1855	. . . . . . . 8 ⊢ Ⅎb∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))
47	45, 46	nfan 1824	. . . . . . 7 ⊢ Ⅎb(k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)))
48		reeanv 2779	. . . . . . . . 9 ⊢ (∃c ∈ k ∃d ∈ k (∃x ∈ ∼ c℘1a = (c ∪ {x}) ∧ ∃y ∈ ∼ d℘1b = (d ∪ {y})) ↔ (∃c ∈ k ∃x ∈ ∼ c℘1a = (c ∪ {x}) ∧ ∃d ∈ k ∃y ∈ ∼ d℘1b = (d ∪ {y})))
49		reeanv 2779	. . . . . . . . . 10 ⊢ (∃x ∈ ∼ c∃y ∈ ∼ d(℘1a = (c ∪ {x}) ∧ ℘1b = (d ∪ {y})) ↔ (∃x ∈ ∼ c℘1a = (c ∪ {x}) ∧ ∃y ∈ ∼ d℘1b = (d ∪ {y})))
50	49	2rexbii 2642	. . . . . . . . 9 ⊢ (∃c ∈ k ∃d ∈ k ∃x ∈ ∼ c∃y ∈ ∼ d(℘1a = (c ∪ {x}) ∧ ℘1b = (d ∪ {y})) ↔ ∃c ∈ k ∃d ∈ k (∃x ∈ ∼ c℘1a = (c ∪ {x}) ∧ ∃y ∈ ∼ d℘1b = (d ∪ {y})))
51		elsuc 4414	. . . . . . . . . 10 ⊢ (℘1a ∈ (k +c 1c) ↔ ∃c ∈ k ∃x ∈ ∼ c℘1a = (c ∪ {x}))
52		elsuc 4414	. . . . . . . . . 10 ⊢ (℘1b ∈ (k +c 1c) ↔ ∃d ∈ k ∃y ∈ ∼ d℘1b = (d ∪ {y}))
53	51, 52	anbi12i 678	. . . . . . . . 9 ⊢ ((℘1a ∈ (k +c 1c) ∧ ℘1b ∈ (k +c 1c)) ↔ (∃c ∈ k ∃x ∈ ∼ c℘1a = (c ∪ {x}) ∧ ∃d ∈ k ∃y ∈ ∼ d℘1b = (d ∪ {y})))
54	48, 50, 53	3bitr4ri 269	. . . . . . . 8 ⊢ ((℘1a ∈ (k +c 1c) ∧ ℘1b ∈ (k +c 1c)) ↔ ∃c ∈ k ∃d ∈ k ∃x ∈ ∼ c∃y ∈ ∼ d(℘1a = (c ∪ {x}) ∧ ℘1b = (d ∪ {y})))
55		vex 2863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ e ∈ V
56		vex 2863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ f ∈ V
57		pw1eq 4144	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (a = e → ℘1a = ℘1e)
58	57	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (a = e → (℘1a ∈ k ↔ ℘1e ∈ k))
59		pw1eq 4144	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (b = f → ℘1b = ℘1f)
60	59	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (b = f → (℘1b ∈ k ↔ ℘1f ∈ k))
61	58, 60	bi2anan9 843	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((a = e ∧ b = f) → ((℘1a ∈ k ∧ ℘1b ∈ k) ↔ (℘1e ∈ k ∧ ℘1f ∈ k)))
62		elequ1 1713	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (a = e → (a ∈ n ↔ e ∈ n))
63		elequ1 1713	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (b = f → (b ∈ n ↔ f ∈ n))
64	62, 63	bi2anan9 843	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((a = e ∧ b = f) → ((a ∈ n ∧ b ∈ n) ↔ (e ∈ n ∧ f ∈ n)))
65	64	rexbidv 2636	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((a = e ∧ b = f) → (∃n ∈ Nn (a ∈ n ∧ b ∈ n) ↔ ∃n ∈ Nn (e ∈ n ∧ f ∈ n)))
66	61, 65	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((a = e ∧ b = f) → (((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ((℘1e ∈ k ∧ ℘1f ∈ k) → ∃n ∈ Nn (e ∈ n ∧ f ∈ n))))
67	66	spc2gv 2943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((e ∈ V ∧ f ∈ V) → (∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) → ((℘1e ∈ k ∧ ℘1f ∈ k) → ∃n ∈ Nn (e ∈ n ∧ f ∈ n))))
68	55, 56, 67	mp2an 653	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) → ((℘1e ∈ k ∧ ℘1f ∈ k) → ∃n ∈ Nn (e ∈ n ∧ f ∈ n)))
69	68	com12 27	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((℘1e ∈ k ∧ ℘1f ∈ k) → (∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) → ∃n ∈ Nn (e ∈ n ∧ f ∈ n)))
70	69	ad2antrl 708	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) → (∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) → ∃n ∈ Nn (e ∈ n ∧ f ∈ n)))
71		peano2 4404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (n ∈ Nn → (n +c 1c) ∈ Nn )
72	71	ad2antrl 708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ (n ∈ Nn ∧ (e ∈ n ∧ f ∈ n))) → (n +c 1c) ∈ Nn )
73		simprrl 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ (n ∈ Nn ∧ (e ∈ n ∧ f ∈ n))) → e ∈ n)
74		simprrl 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) → ¬ z ∈ e)
75	74	adantr 451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ (n ∈ Nn ∧ (e ∈ n ∧ f ∈ n))) → ¬ z ∈ e)
76		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ z ∈ V
77	76	elsuci 4415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((e ∈ n ∧ ¬ z ∈ e) → (e ∪ {z}) ∈ (n +c 1c))
78	73, 75, 77	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ (n ∈ Nn ∧ (e ∈ n ∧ f ∈ n))) → (e ∪ {z}) ∈ (n +c 1c))
79		simprrr 741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ (n ∈ Nn ∧ (e ∈ n ∧ f ∈ n))) → f ∈ n)
80		simprrr 741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) → ¬ w ∈ f)
81	80	adantr 451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ (n ∈ Nn ∧ (e ∈ n ∧ f ∈ n))) → ¬ w ∈ f)
82		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ w ∈ V
83	82	elsuci 4415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f ∈ n ∧ ¬ w ∈ f) → (f ∪ {w}) ∈ (n +c 1c))
84	79, 81, 83	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ (n ∈ Nn ∧ (e ∈ n ∧ f ∈ n))) → (f ∪ {w}) ∈ (n +c 1c))
85		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (m = (n +c 1c) → ((e ∪ {z}) ∈ m ↔ (e ∪ {z}) ∈ (n +c 1c)))
86		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (m = (n +c 1c) → ((f ∪ {w}) ∈ m ↔ (f ∪ {w}) ∈ (n +c 1c)))
87	85, 86	anbi12d 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (m = (n +c 1c) → (((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m) ↔ ((e ∪ {z}) ∈ (n +c 1c) ∧ (f ∪ {w}) ∈ (n +c 1c))))
88	87	rspcev 2956	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((n +c 1c) ∈ Nn ∧ ((e ∪ {z}) ∈ (n +c 1c) ∧ (f ∪ {w}) ∈ (n +c 1c))) → ∃m ∈ Nn ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m))
89	72, 78, 84, 88	syl12anc 1180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ (n ∈ Nn ∧ (e ∈ n ∧ f ∈ n))) → ∃m ∈ Nn ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m))
90	89	expr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ n ∈ Nn ) → ((e ∈ n ∧ f ∈ n) → ∃m ∈ Nn ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m)))
91	90	rexlimdva 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) → (∃n ∈ Nn (e ∈ n ∧ f ∈ n) → ∃m ∈ Nn ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m)))
92	70, 91	syld 40	. . . . . . . . . . . . . . . . . 18 ⊢ ((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) → (∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) → ∃m ∈ Nn ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m)))
93	92	imp 418	. . . . . . . . . . . . . . . . 17 ⊢ (((k ∈ Nn ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) → ∃m ∈ Nn ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m))
94	93	an32s 779	. . . . . . . . . . . . . . . 16 ⊢ (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) → ∃m ∈ Nn ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m))
95		eleq1 2413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (c = ℘1e → (c ∈ k ↔ ℘1e ∈ k))
96	95	3ad2ant2 977	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) → (c ∈ k ↔ ℘1e ∈ k))
97		eleq1 2413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (d = ℘1f → (d ∈ k ↔ ℘1f ∈ k))
98	97	3ad2ant2 977	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w}) → (d ∈ k ↔ ℘1f ∈ k))
99	96, 98	bi2anan9 843	. . . . . . . . . . . . . . . . . . 19 ⊢ (((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → ((c ∈ k ∧ d ∈ k) ↔ (℘1e ∈ k ∧ ℘1f ∈ k)))
100		compleq 3244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (c = ℘1e → ∼ c = ∼ ℘1e)
101		eleq12 2415	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((x = {z} ∧ ∼ c = ∼ ℘1e) → (x ∈ ∼ c ↔ {z} ∈ ∼ ℘1e))
102	100, 101	sylan2 460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((x = {z} ∧ c = ℘1e) → (x ∈ ∼ c ↔ {z} ∈ ∼ ℘1e))
103		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {z} ∈ V
104	103	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({z} ∈ ∼ ℘1e ↔ ¬ {z} ∈ ℘1e)
105		snelpw1 4147	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({z} ∈ ℘1e ↔ z ∈ e)
106	104, 105	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({z} ∈ ∼ ℘1e ↔ ¬ z ∈ e)
107	102, 106	syl6bb 252	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((x = {z} ∧ c = ℘1e) → (x ∈ ∼ c ↔ ¬ z ∈ e))
108	107	ancoms 439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((c = ℘1e ∧ x = {z}) → (x ∈ ∼ c ↔ ¬ z ∈ e))
109	108	3adant1 973	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) → (x ∈ ∼ c ↔ ¬ z ∈ e))
110		compleq 3244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (d = ℘1f → ∼ d = ∼ ℘1f)
111		eleq12 2415	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((y = {w} ∧ ∼ d = ∼ ℘1f) → (y ∈ ∼ d ↔ {w} ∈ ∼ ℘1f))
112	110, 111	sylan2 460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y = {w} ∧ d = ℘1f) → (y ∈ ∼ d ↔ {w} ∈ ∼ ℘1f))
113		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {w} ∈ V
114	113	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({w} ∈ ∼ ℘1f ↔ ¬ {w} ∈ ℘1f)
115		snelpw1 4147	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ({w} ∈ ℘1f ↔ w ∈ f)
116	114, 115	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({w} ∈ ∼ ℘1f ↔ ¬ w ∈ f)
117	112, 116	syl6bb 252	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y = {w} ∧ d = ℘1f) → (y ∈ ∼ d ↔ ¬ w ∈ f))
118	117	ancoms 439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((d = ℘1f ∧ y = {w}) → (y ∈ ∼ d ↔ ¬ w ∈ f))
119	118	3adant1 973	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w}) → (y ∈ ∼ d ↔ ¬ w ∈ f))
120	109, 119	bi2anan9 843	. . . . . . . . . . . . . . . . . . 19 ⊢ (((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → ((x ∈ ∼ c ∧ y ∈ ∼ d) ↔ (¬ z ∈ e ∧ ¬ w ∈ f)))
121	99, 120	anbi12d 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → (((c ∈ k ∧ d ∈ k) ∧ (x ∈ ∼ c ∧ y ∈ ∼ d)) ↔ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))))
122	121	anbi2d 684	. . . . . . . . . . . . . . . . 17 ⊢ (((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((c ∈ k ∧ d ∈ k) ∧ (x ∈ ∼ c ∧ y ∈ ∼ d))) ↔ ((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f)))))
123		eleq1 2413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (a = (e ∪ {z}) → (a ∈ m ↔ (e ∪ {z}) ∈ m))
124	123	3ad2ant1 976	. . . . . . . . . . . . . . . . . . 19 ⊢ ((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) → (a ∈ m ↔ (e ∪ {z}) ∈ m))
125		eleq1 2413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (b = (f ∪ {w}) → (b ∈ m ↔ (f ∪ {w}) ∈ m))
126	125	3ad2ant1 976	. . . . . . . . . . . . . . . . . . 19 ⊢ ((b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w}) → (b ∈ m ↔ (f ∪ {w}) ∈ m))
127	124, 126	bi2anan9 843	. . . . . . . . . . . . . . . . . 18 ⊢ (((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → ((a ∈ m ∧ b ∈ m) ↔ ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m)))
128	127	rexbidv 2636	. . . . . . . . . . . . . . . . 17 ⊢ (((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → (∃m ∈ Nn (a ∈ m ∧ b ∈ m) ↔ ∃m ∈ Nn ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m)))
129	122, 128	imbi12d 311	. . . . . . . . . . . . . . . 16 ⊢ (((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → ((((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((c ∈ k ∧ d ∈ k) ∧ (x ∈ ∼ c ∧ y ∈ ∼ d))) → ∃m ∈ Nn (a ∈ m ∧ b ∈ m)) ↔ (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((℘1e ∈ k ∧ ℘1f ∈ k) ∧ (¬ z ∈ e ∧ ¬ w ∈ f))) → ∃m ∈ Nn ((e ∪ {z}) ∈ m ∧ (f ∪ {w}) ∈ m))))
130	94, 129	mpbiri 224	. . . . . . . . . . . . . . 15 ⊢ (((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((c ∈ k ∧ d ∈ k) ∧ (x ∈ ∼ c ∧ y ∈ ∼ d))) → ∃m ∈ Nn (a ∈ m ∧ b ∈ m)))
131	130	com12 27	. . . . . . . . . . . . . 14 ⊢ (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((c ∈ k ∧ d ∈ k) ∧ (x ∈ ∼ c ∧ y ∈ ∼ d))) → (((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → ∃m ∈ Nn (a ∈ m ∧ b ∈ m)))
132	131	exlimdvv 1637	. . . . . . . . . . . . 13 ⊢ (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((c ∈ k ∧ d ∈ k) ∧ (x ∈ ∼ c ∧ y ∈ ∼ d))) → (∃z∃w((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → ∃m ∈ Nn (a ∈ m ∧ b ∈ m)))
133	132	exlimdvv 1637	. . . . . . . . . . . 12 ⊢ (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((c ∈ k ∧ d ∈ k) ∧ (x ∈ ∼ c ∧ y ∈ ∼ d))) → (∃e∃f∃z∃w((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) → ∃m ∈ Nn (a ∈ m ∧ b ∈ m)))
134		eeanv 1913	. . . . . . . . . . . . 13 ⊢ (∃e∃f(∃z(a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ ∃w(b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) ↔ (∃e∃z(a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ ∃f∃w(b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})))
135		eeanv 1913	. . . . . . . . . . . . . 14 ⊢ (∃z∃w((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) ↔ (∃z(a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ ∃w(b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})))
136	135	2exbii 1583	. . . . . . . . . . . . 13 ⊢ (∃e∃f∃z∃w((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})) ↔ ∃e∃f(∃z(a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ ∃w(b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})))
137		vex 2863	. . . . . . . . . . . . . . 15 ⊢ c ∈ V
138		vex 2863	. . . . . . . . . . . . . . 15 ⊢ x ∈ V
139	137, 138	pw1eqadj 4333	. . . . . . . . . . . . . 14 ⊢ (℘1a = (c ∪ {x}) ↔ ∃e∃z(a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}))
140		vex 2863	. . . . . . . . . . . . . . 15 ⊢ d ∈ V
141		vex 2863	. . . . . . . . . . . . . . 15 ⊢ y ∈ V
142	140, 141	pw1eqadj 4333	. . . . . . . . . . . . . 14 ⊢ (℘1b = (d ∪ {y}) ↔ ∃f∃w(b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w}))
143	139, 142	anbi12i 678	. . . . . . . . . . . . 13 ⊢ ((℘1a = (c ∪ {x}) ∧ ℘1b = (d ∪ {y})) ↔ (∃e∃z(a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ ∃f∃w(b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})))
144	134, 136, 143	3bitr4ri 269	. . . . . . . . . . . 12 ⊢ ((℘1a = (c ∪ {x}) ∧ ℘1b = (d ∪ {y})) ↔ ∃e∃f∃z∃w((a = (e ∪ {z}) ∧ c = ℘1e ∧ x = {z}) ∧ (b = (f ∪ {w}) ∧ d = ℘1f ∧ y = {w})))
145		elequ2 1715	. . . . . . . . . . . . . 14 ⊢ (n = m → (a ∈ n ↔ a ∈ m))
146		elequ2 1715	. . . . . . . . . . . . . 14 ⊢ (n = m → (b ∈ n ↔ b ∈ m))
147	145, 146	anbi12d 691	. . . . . . . . . . . . 13 ⊢ (n = m → ((a ∈ n ∧ b ∈ n) ↔ (a ∈ m ∧ b ∈ m)))
148	147	cbvrexv 2837	. . . . . . . . . . . 12 ⊢ (∃n ∈ Nn (a ∈ n ∧ b ∈ n) ↔ ∃m ∈ Nn (a ∈ m ∧ b ∈ m))
149	133, 144, 148	3imtr4g 261	. . . . . . . . . . 11 ⊢ (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ ((c ∈ k ∧ d ∈ k) ∧ (x ∈ ∼ c ∧ y ∈ ∼ d))) → ((℘1a = (c ∪ {x}) ∧ ℘1b = (d ∪ {y})) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)))
150	149	expr 598	. . . . . . . . . 10 ⊢ (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ (c ∈ k ∧ d ∈ k)) → ((x ∈ ∼ c ∧ y ∈ ∼ d) → ((℘1a = (c ∪ {x}) ∧ ℘1b = (d ∪ {y})) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
151	150	rexlimdvv 2745	. . . . . . . . 9 ⊢ (((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) ∧ (c ∈ k ∧ d ∈ k)) → (∃x ∈ ∼ c∃y ∈ ∼ d(℘1a = (c ∪ {x}) ∧ ℘1b = (d ∪ {y})) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)))
152	151	rexlimdvva 2746	. . . . . . . 8 ⊢ ((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) → (∃c ∈ k ∃d ∈ k ∃x ∈ ∼ c∃y ∈ ∼ d(℘1a = (c ∪ {x}) ∧ ℘1b = (d ∪ {y})) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)))
153	54, 152	syl5bi 208	. . . . . . 7 ⊢ ((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) → ((℘1a ∈ (k +c 1c) ∧ ℘1b ∈ (k +c 1c)) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)))
154	47, 153	alrimi 1765	. . . . . 6 ⊢ ((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) → ∀b((℘1a ∈ (k +c 1c) ∧ ℘1b ∈ (k +c 1c)) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)))
155	44, 154	alrimi 1765	. . . . 5 ⊢ ((k ∈ Nn ∧ ∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))) → ∀a∀b((℘1a ∈ (k +c 1c) ∧ ℘1b ∈ (k +c 1c)) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)))
156	155	ex 423	. . . 4 ⊢ (k ∈ Nn → (∀a∀b((℘1a ∈ k ∧ ℘1b ∈ k) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) → ∀a∀b((℘1a ∈ (k +c 1c) ∧ ℘1b ∈ (k +c 1c)) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))))
157	1, 6, 11, 16, 21, 41, 156	finds 4412	. . 3 ⊢ (M ∈ Nn → ∀a∀b((℘1a ∈ M ∧ ℘1b ∈ M) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)))
158		elex 2868	. . . . . 6 ⊢ (℘1A ∈ M → ℘1A ∈ V)
159		pw1exb 4327	. . . . . 6 ⊢ (℘1A ∈ V ↔ A ∈ V)
160	158, 159	sylib 188	. . . . 5 ⊢ (℘1A ∈ M → A ∈ V)
161		elex 2868	. . . . . 6 ⊢ (℘1B ∈ M → ℘1B ∈ V)
162		pw1exb 4327	. . . . . 6 ⊢ (℘1B ∈ V ↔ B ∈ V)
163	161, 162	sylib 188	. . . . 5 ⊢ (℘1B ∈ M → B ∈ V)
164		pw1eq 4144	. . . . . . . . 9 ⊢ (a = A → ℘1a = ℘1A)
165	164	eleq1d 2419	. . . . . . . 8 ⊢ (a = A → (℘1a ∈ M ↔ ℘1A ∈ M))
166		pw1eq 4144	. . . . . . . . 9 ⊢ (b = B → ℘1b = ℘1B)
167	166	eleq1d 2419	. . . . . . . 8 ⊢ (b = B → (℘1b ∈ M ↔ ℘1B ∈ M))
168	165, 167	bi2anan9 843	. . . . . . 7 ⊢ ((a = A ∧ b = B) → ((℘1a ∈ M ∧ ℘1b ∈ M) ↔ (℘1A ∈ M ∧ ℘1B ∈ M)))
169		eleq1 2413	. . . . . . . . 9 ⊢ (a = A → (a ∈ n ↔ A ∈ n))
170		eleq1 2413	. . . . . . . . 9 ⊢ (b = B → (b ∈ n ↔ B ∈ n))
171	169, 170	bi2anan9 843	. . . . . . . 8 ⊢ ((a = A ∧ b = B) → ((a ∈ n ∧ b ∈ n) ↔ (A ∈ n ∧ B ∈ n)))
172	171	rexbidv 2636	. . . . . . 7 ⊢ ((a = A ∧ b = B) → (∃n ∈ Nn (a ∈ n ∧ b ∈ n) ↔ ∃n ∈ Nn (A ∈ n ∧ B ∈ n)))
173	168, 172	imbi12d 311	. . . . . 6 ⊢ ((a = A ∧ b = B) → (((℘1a ∈ M ∧ ℘1b ∈ M) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) ↔ ((℘1A ∈ M ∧ ℘1B ∈ M) → ∃n ∈ Nn (A ∈ n ∧ B ∈ n))))
174	173	spc2gv 2943	. . . . 5 ⊢ ((A ∈ V ∧ B ∈ V) → (∀a∀b((℘1a ∈ M ∧ ℘1b ∈ M) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) → ((℘1A ∈ M ∧ ℘1B ∈ M) → ∃n ∈ Nn (A ∈ n ∧ B ∈ n))))
175	160, 163, 174	syl2an 463	. . . 4 ⊢ ((℘1A ∈ M ∧ ℘1B ∈ M) → (∀a∀b((℘1a ∈ M ∧ ℘1b ∈ M) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) → ((℘1A ∈ M ∧ ℘1B ∈ M) → ∃n ∈ Nn (A ∈ n ∧ B ∈ n))))
176	175	pm2.43b 46	. . 3 ⊢ (∀a∀b((℘1a ∈ M ∧ ℘1b ∈ M) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n)) → ((℘1A ∈ M ∧ ℘1B ∈ M) → ∃n ∈ Nn (A ∈ n ∧ B ∈ n)))
177	157, 176	syl 15	. 2 ⊢ (M ∈ Nn → ((℘1A ∈ M ∧ ℘1B ∈ M) → ∃n ∈ Nn (A ∈ n ∧ B ∈ n)))
178	177	3impib 1149	1 ⊢ ((M ∈ Nn ∧ ℘1A ∈ M ∧ ℘1B ∈ M) → ∃n ∈ Nn (A ∈ n ∧ B ∈ n))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2616  Vcvv 2860   ∼ ccompl 3206   ∪ cun 3208  ∅c0 3551  {csn 3738  1_cc1c 4135  ℘₁cpw1 4136   Nn cnnc 4374  0_cc0c 4375   +_c cplc 4376

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-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-symdif 3217  df-ss 3260  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-0c 4378  df-addc 4379  df-nnc 4380

This theorem is referenced by:  tfin11  4494  sfin112  4530  sfindbl  4531  sfinltfin  4536