Theorem unifiOLD 4570

Description: The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144.

Assertion

Ref	Expression
unifiOLD	⊢ ((∃n ∈ ω A ≈ n ⋀ ∀x ∈ A ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪A ≈ n)

Distinct variable group:   x,n,A

Proof of Theorem unifiOLD

Step	Hyp	Ref	Expression
1		breq2 2628	. . . 4 ⊢ (n = m → (A ≈ n ↔ A ≈ m))
2	1	cbvrexv 1804	. . 3 ⊢ (∃n ∈ ω A ≈ n ↔ ∃m ∈ ω A ≈ m)
3		breq2 2628	. . . . . . . . 9 ⊢ (m = ∅ → (y ≈ m ↔ y ≈ ∅))
4	3	anbi1d 619	. . . . . . . 8 ⊢ (m = ∅ → ((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (y ≈ ∅ ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)))
5	4	imbi1d 615	. . . . . . 7 ⊢ (m = ∅ → (((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ((y ≈ ∅ ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)))
6	5	albidv 1280	. . . . . 6 ⊢ (m = ∅ → (∀y((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ∀y((y ≈ ∅ ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)))
7		breq2 2628	. . . . . . . . 9 ⊢ (m = k → (y ≈ m ↔ y ≈ k))
8	7	anbi1d 619	. . . . . . . 8 ⊢ (m = k → ((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)))
9	8	imbi1d 615	. . . . . . 7 ⊢ (m = k → (((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ((y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)))
10	9	albidv 1280	. . . . . 6 ⊢ (m = k → (∀y((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ∀y((y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)))
11		breq2 2628	. . . . . . . . 9 ⊢ (m = suc k → (y ≈ m ↔ y ≈ suc k))
12	11	anbi1d 619	. . . . . . . 8 ⊢ (m = suc k → ((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (y ≈ suc k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)))
13	12	imbi1d 615	. . . . . . 7 ⊢ (m = suc k → (((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ((y ≈ suc k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)))
14	13	albidv 1280	. . . . . 6 ⊢ (m = suc k → (∀y((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ∀y((y ≈ suc k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)))
15		en0 4429	. . . . . . . . 9 ⊢ (y ≈ ∅ ↔ y = ∅)
16		unieq 2514	. . . . . . . . . . 11 ⊢ (y = ∅ → ∪y = ∪∅)
17		uni0 2529	. . . . . . . . . . . 12 ⊢ ∪∅ = ∅
18		0ex 2716	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
19	18	enref 4397	. . . . . . . . . . . 12 ⊢ ∅ ≈ ∅
20	17, 19	eqbrtr 2639	. . . . . . . . . . 11 ⊢ ∪∅ ≈ ∅
21	16, 20	syl6eqbr 2657	. . . . . . . . . 10 ⊢ (y = ∅ → ∪y ≈ ∅)
22		peano1 3155	. . . . . . . . . . 11 ⊢ ∅ ∈ ω
23		breq2 2628	. . . . . . . . . . . 12 ⊢ (n = ∅ → (∪y ≈ n ↔ ∪y ≈ ∅))
24	23	rcla4ev 1880	. . . . . . . . . . 11 ⊢ ((∅ ∈ ω ⋀ ∪y ≈ ∅) → ∃n ∈ ω ∪y ≈ n)
25	22, 24	mpan 697	. . . . . . . . . 10 ⊢ (∪y ≈ ∅ → ∃n ∈ ω ∪y ≈ n)
26	21, 25	syl 10	. . . . . . . . 9 ⊢ (y = ∅ → ∃n ∈ ω ∪y ≈ n)
27	15, 26	sylbi 199	. . . . . . . 8 ⊢ (y ≈ ∅ → ∃n ∈ ω ∪y ≈ n)
28	27	adantr 391	. . . . . . 7 ⊢ ((y ≈ ∅ ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)
29	28	ax-gen 965	. . . . . 6 ⊢ ∀y((y ≈ ∅ ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)
30		breq1 2627	. . . . . . . . . . 11 ⊢ (y = z → (y ≈ k ↔ z ≈ k))
31		raleq1 1789	. . . . . . . . . . 11 ⊢ (y = z → (∀x ∈ y ∃n ∈ ω x ≈ n ↔ ∀x ∈ z ∃n ∈ ω x ≈ n))
32	30, 31	anbi12d 630	. . . . . . . . . 10 ⊢ (y = z → ((y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n)))
33		unieq 2514	. . . . . . . . . . . 12 ⊢ (y = z → ∪y = ∪z)
34	33	breq1d 2634	. . . . . . . . . . 11 ⊢ (y = z → (∪y ≈ n ↔ ∪z ≈ n))
35	34	rexbidv 1667	. . . . . . . . . 10 ⊢ (y = z → (∃n ∈ ω ∪y ≈ n ↔ ∃n ∈ ω ∪z ≈ n))
36	32, 35	imbi12d 628	. . . . . . . . 9 ⊢ (y = z → (((y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n)))
37	36	cbvalv 1316	. . . . . . . 8 ⊢ (∀y((y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n))
38		visset 1816	. . . . . . . . . . . . . . 15 ⊢ k ∈ V
39	38	sucex 3056	. . . . . . . . . . . . . 14 ⊢ suc k ∈ V
40	39	ensym 4418	. . . . . . . . . . . . 13 ⊢ (y ≈ suc k → suc k ≈ y)
41		visset 1816	. . . . . . . . . . . . . 14 ⊢ y ∈ V
42	41	bren 4383	. . . . . . . . . . . . 13 ⊢ (suc k ≈ y ↔ ∃f f:suc k–1-1-onto→y)
43	40, 42	sylib 198	. . . . . . . . . . . 12 ⊢ (y ≈ suc k → ∃f f:suc k–1-1-onto→y)
44		unfiOLD 4564	. . . . . . . . . . . . . . . 16 ⊢ ((∃n ∈ ω ∪(f “ k) ≈ n ⋀ ∃n ∈ ω (f ‘k) ≈ n) → ∃n ∈ ω (∪(f “ k) ∪ (f ‘k)) ≈ n)
45		visset 1816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ f ∈ V
46		imaexg 3422	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f ∈ V → (f “ k) ∈ V)
47	45, 46	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f “ k) ∈ V
48		breq1 2627	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z = (f “ k) → (z ≈ k ↔ (f “ k) ≈ k))
49		raleq1 1789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z = (f “ k) → (∀x ∈ z ∃n ∈ ω x ≈ n ↔ ∀x ∈ (f “ k)∃n ∈ ω x ≈ n))
50	48, 49	anbi12d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z = (f “ k) → ((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) ↔ ((f “ k) ≈ k ⋀ ∀x ∈ (f “ k)∃n ∈ ω x ≈ n)))
51		unieq 2514	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (z = (f “ k) → ∪z = ∪(f “ k))
52	51	breq1d 2634	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z = (f “ k) → (∪z ≈ n ↔ ∪(f “ k) ≈ n))
53	52	rexbidv 1667	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z = (f “ k) → (∃n ∈ ω ∪z ≈ n ↔ ∃n ∈ ω ∪(f “ k) ≈ n))
54	50, 53	imbi12d 628	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z = (f “ k) → (((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) ↔ (((f “ k) ≈ k ⋀ ∀x ∈ (f “ k)∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪(f “ k) ≈ n)))
55	47, 54	cla4v 1871	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) → (((f “ k) ≈ k ⋀ ∀x ∈ (f “ k)∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪(f “ k) ≈ n))
56	55	imp 350	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) ⋀ ((f “ k) ≈ k ⋀ ∀x ∈ (f “ k)∃n ∈ ω x ≈ n)) → ∃n ∈ ω ∪(f “ k) ≈ n)
57		f1of1 3694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:suc k–1-1-onto→y → f:suc k–1-1→y)
58		sssucid 3053	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ k ⊆ suc k
59		f1ores 3709	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f:suc k–1-1→y ⋀ k ⊆ suc k) → (f ↾ k):k–1-1-onto→(f “ k))
60	58, 59	mpan2 698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:suc k–1-1→y → (f ↾ k):k–1-1-onto→(f “ k))
61	38	f1oen 4404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((f ↾ k):k–1-1-onto→(f “ k) → k ≈ (f “ k))
62	57, 60, 61	3syl 20	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f:suc k–1-1-onto→y → k ≈ (f “ k))
63	47	ensym 4418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (k ≈ (f “ k) → (f “ k) ≈ k)
64	62, 63	syl 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f:suc k–1-1-onto→y → (f “ k) ≈ k)
65	64	adantr 391	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f:suc k–1-1-onto→y ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → (f “ k) ≈ k)
66		ssun1 2196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f “ k) ⊆ ((f “ k) ∪ {(f ‘k)})
67	66	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:suc k–1-1-onto→y → (f “ k) ⊆ ((f “ k) ∪ {(f ‘k)}))
68		f1ofn 3696	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc k–1-1-onto→y → f Fn suc k)
69	38	sucid 3057	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ k ∈ suc k
70		fnsnfv 3773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f Fn suc k ⋀ k ∈ suc k) → {(f ‘k)} = (f “ {k}))
71	69, 70	mpan2 698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f Fn suc k → {(f ‘k)} = (f “ {k}))
72	68, 71	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f:suc k–1-1-onto→y → {(f ‘k)} = (f “ {k}))
73	72	uneq2d 2187	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:suc k–1-1-onto→y → ((f “ k) ∪ {(f ‘k)}) = ((f “ k) ∪ (f “ {k})))
74		df-suc 2960	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ suc k = (k ∪ {k})
75		imaeq2 3408	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (suc k = (k ∪ {k}) → (f “ suc k) = (f “ (k ∪ {k})))
76	74, 75	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f “ suc k) = (f “ (k ∪ {k}))
77		imaun 3466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f “ (k ∪ {k})) = ((f “ k) ∪ (f “ {k}))
78	76, 77	eqtr2 1499	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f “ k) ∪ (f “ {k})) = (f “ suc k)
79	73, 78	syl6eq 1526	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f:suc k–1-1-onto→y → ((f “ k) ∪ {(f ‘k)}) = (f “ suc k))
80		f1ofo 3701	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:suc k–1-1-onto→y → f:suc k–onto→y)
81		foima 3682	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:suc k–onto→y → (f “ suc k) = y)
82	80, 81	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f:suc k–1-1-onto→y → (f “ suc k) = y)
83	79, 82	eqtrd 1510	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:suc k–1-1-onto→y → ((f “ k) ∪ {(f ‘k)}) = y)
84	67, 83	sseqtrd 2100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f:suc k–1-1-onto→y → (f “ k) ⊆ y)
85		ssralv 2117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((f “ k) ⊆ y → (∀x ∈ y ∃n ∈ ω x ≈ n → ∀x ∈ (f “ k)∃n ∈ ω x ≈ n))
86	84, 85	syl 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f:suc k–1-1-onto→y → (∀x ∈ y ∃n ∈ ω x ≈ n → ∀x ∈ (f “ k)∃n ∈ ω x ≈ n))
87	86	imp 350	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f:suc k–1-1-onto→y ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∀x ∈ (f “ k)∃n ∈ ω x ≈ n)
88	65, 87	jca 288	. . . . . . . . . . . . . . . . . 18 ⊢ ((f:suc k–1-1-onto→y ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ((f “ k) ≈ k ⋀ ∀x ∈ (f “ k)∃n ∈ ω x ≈ n))
89	56, 88	sylan2 453	. . . . . . . . . . . . . . . . 17 ⊢ ((∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) ⋀ (f:suc k–1-1-onto→y ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)) → ∃n ∈ ω ∪(f “ k) ≈ n)
90	89	an1s 488	. . . . . . . . . . . . . . . 16 ⊢ ((f:suc k–1-1-onto→y ⋀ (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)) → ∃n ∈ ω ∪(f “ k) ≈ n)
91		breq1 2627	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = (f ‘k) → (x ≈ n ↔ (f ‘k) ≈ n))
92	91	rexbidv 1667	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = (f ‘k) → (∃n ∈ ω x ≈ n ↔ ∃n ∈ ω (f ‘k) ≈ n))
93	92	rcla4va 1878	. . . . . . . . . . . . . . . . . 18 ⊢ (((f ‘k) ∈ y ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω (f ‘k) ≈ n)
94		f1of 3695	. . . . . . . . . . . . . . . . . . 19 ⊢ (f:suc k–1-1-onto→y → f:suc k–→y)
95		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f:suc k–→y ⋀ k ∈ suc k) → (f ‘k) ∈ y)
96	69, 95	mpan2 698	. . . . . . . . . . . . . . . . . . 19 ⊢ (f:suc k–→y → (f ‘k) ∈ y)
97	94, 96	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ (f:suc k–1-1-onto→y → (f ‘k) ∈ y)
98	93, 97	sylan 450	. . . . . . . . . . . . . . . . 17 ⊢ ((f:suc k–1-1-onto→y ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω (f ‘k) ≈ n)
99	98	adantrl 396	. . . . . . . . . . . . . . . 16 ⊢ ((f:suc k–1-1-onto→y ⋀ (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)) → ∃n ∈ ω (f ‘k) ≈ n)
100	44, 90, 99	sylanc 473	. . . . . . . . . . . . . . 15 ⊢ ((f:suc k–1-1-onto→y ⋀ (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)) → ∃n ∈ ω (∪(f “ k) ∪ (f ‘k)) ≈ n)
101	83	unieqd 2516	. . . . . . . . . . . . . . . . . . 19 ⊢ (f:suc k–1-1-onto→y → ∪((f “ k) ∪ {(f ‘k)}) = ∪y)
102		uniun 2523	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪((f “ k) ∪ {(f ‘k)}) = (∪(f “ k) ∪ ∪{(f ‘k)})
103		fvex 3738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f ‘k) ∈ V
104	103	unisn 2521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪{(f ‘k)} = (f ‘k)
105	104	uneq2i 2184	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪(f “ k) ∪ ∪{(f ‘k)}) = (∪(f “ k) ∪ (f ‘k))
106	102, 105	eqtr2 1499	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪(f “ k) ∪ (f ‘k)) = ∪((f “ k) ∪ {(f ‘k)})
107	101, 106	syl5eq 1522	. . . . . . . . . . . . . . . . . 18 ⊢ (f:suc k–1-1-onto→y → (∪(f “ k) ∪ (f ‘k)) = ∪y)
108	107	breq1d 2634	. . . . . . . . . . . . . . . . 17 ⊢ (f:suc k–1-1-onto→y → ((∪(f “ k) ∪ (f ‘k)) ≈ n ↔ ∪y ≈ n))
109	108	rexbidv 1667	. . . . . . . . . . . . . . . 16 ⊢ (f:suc k–1-1-onto→y → (∃n ∈ ω (∪(f “ k) ∪ (f ‘k)) ≈ n ↔ ∃n ∈ ω ∪y ≈ n))
110	109	adantr 391	. . . . . . . . . . . . . . 15 ⊢ ((f:suc k–1-1-onto→y ⋀ (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)) → (∃n ∈ ω (∪(f “ k) ∪ (f ‘k)) ≈ n ↔ ∃n ∈ ω ∪y ≈ n))
111	100, 110	mpbid 195	. . . . . . . . . . . . . 14 ⊢ ((f:suc k–1-1-onto→y ⋀ (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)) → ∃n ∈ ω ∪y ≈ n)
112	111	exp32 379	. . . . . . . . . . . . 13 ⊢ (f:suc k–1-1-onto→y → (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) → (∀x ∈ y ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪y ≈ n)))
113	112	19.23aiv 1297	. . . . . . . . . . . 12 ⊢ (∃f f:suc k–1-1-onto→y → (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) → (∀x ∈ y ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪y ≈ n)))
114	43, 113	syl 10	. . . . . . . . . . 11 ⊢ (y ≈ suc k → (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) → (∀x ∈ y ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪y ≈ n)))
115	114	com12 11	. . . . . . . . . 10 ⊢ (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) → (y ≈ suc k → (∀x ∈ y ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪y ≈ n)))
116	115	imp3a 361	. . . . . . . . 9 ⊢ (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) → ((y ≈ suc k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n))
117	116	19.21aiv 1288	. . . . . . . 8 ⊢ (∀z((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪z ≈ n) → ∀y((y ≈ suc k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n))
118	37, 117	sylbi 199	. . . . . . 7 ⊢ (∀y((y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) → ∀y((y ≈ suc k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n))
119	118	a1i 8	. . . . . 6 ⊢ (k ∈ ω → (∀y((y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) → ∀y((y ≈ suc k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)))
120	6, 10, 14, 29, 119	finds1 3165	. . . . 5 ⊢ (m ∈ ω → ∀y((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n))
121		relen 4378	. . . . . . . 8 ⊢ Rel ≈
122	121	brrelexi 3214	. . . . . . 7 ⊢ (A ≈ m → A ∈ V)
123		breq1 2627	. . . . . . . . . . 11 ⊢ (y = A → (y ≈ m ↔ A ≈ m))
124		raleq1 1789	. . . . . . . . . . 11 ⊢ (y = A → (∀x ∈ y ∃n ∈ ω x ≈ n ↔ ∀x ∈ A ∃n ∈ ω x ≈ n))
125	123, 124	anbi12d 630	. . . . . . . . . 10 ⊢ (y = A → ((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (A ≈ m ⋀ ∀x ∈ A ∃n ∈ ω x ≈ n)))
126		unieq 2514	. . . . . . . . . . . 12 ⊢ (y = A → ∪y = ∪A)
127	126	breq1d 2634	. . . . . . . . . . 11 ⊢ (y = A → (∪y ≈ n ↔ ∪A ≈ n))
128	127	rexbidv 1667	. . . . . . . . . 10 ⊢ (y = A → (∃n ∈ ω ∪y ≈ n ↔ ∃n</