ncfinlower - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > ncfinlower		GIF version

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ 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 proof depends on 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 proof 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 used by: tfin11 4494 sfin112 4530 sfindbl 4531 sfinltfin 4536

W3C validator