Theorem unifi 4550

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

Assertion

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

Distinct variable group:   x,n,A

Proof of Theorem unifi

Step	Hyp	Ref	Expression
1		breq2 2619	. . . 4 ⊢ (n = m → (A ≈ n ↔ A ≈ m))
2	1	cbvrexv 1797	. . 3 ⊢ (∃n ∈ ω A ≈ n ↔ ∃m ∈ ω A ≈ m)
3		breq2 2619	. . . . . . . . 9 ⊢ (m = ∅ → (y ≈ m ↔ y ≈ ∅))
4	3	anbi1d 616	. . . . . . . 8 ⊢ (m = ∅ → ((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (y ≈ ∅ ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)))
5	4	imbi1d 612	. . . . . . 7 ⊢ (m = ∅ → (((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ((y ≈ ∅ ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)))
6	5	albidv 1276	. . . . . 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 2619	. . . . . . . . 9 ⊢ (m = k → (y ≈ m ↔ y ≈ k))
8	7	anbi1d 616	. . . . . . . 8 ⊢ (m = k → ((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)))
9	8	imbi1d 612	. . . . . . 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 1276	. . . . . 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 2619	. . . . . . . . 9 ⊢ (m = suc k → (y ≈ m ↔ y ≈ suc k))
12	11	anbi1d 616	. . . . . . . 8 ⊢ (m = suc k → ((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (y ≈ suc k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n)))
13	12	imbi1d 612	. . . . . . 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 1276	. . . . . 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 4421	. . . . . . . . 9 ⊢ (y ≈ ∅ ↔ y = ∅)
16		unieq 2506	. . . . . . . . . . 11 ⊢ (y = ∅ → ∪y = ∪∅)
17		uni0 2521	. . . . . . . . . . . 12 ⊢ ∪∅ = ∅
18		0ex 2707	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
19	18	enref 4389	. . . . . . . . . . . 12 ⊢ ∅ ≈ ∅
20	17, 19	eqbrtr 2630	. . . . . . . . . . 11 ⊢ ∪∅ ≈ ∅
21	16, 20	syl6eqbr 2648	. . . . . . . . . 10 ⊢ (y = ∅ → ∪y ≈ ∅)
22		peano1 3149	. . . . . . . . . . 11 ⊢ ∅ ∈ ω
23		breq2 2619	. . . . . . . . . . . 12 ⊢ (n = ∅ → (∪y ≈ n ↔ ∪y ≈ ∅))
24	23	rcla4ev 1873	. . . . . . . . . . 11 ⊢ ((∅ ∈ ω ⋀ ∪y ≈ ∅) → ∃n ∈ ω ∪y ≈ n)
25	22, 24	mpan 694	. . . . . . . . . 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 389	. . . . . . 7 ⊢ ((y ≈ ∅ ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)
29	28	ax-gen 961	. . . . . 6 ⊢ ∀y((y ≈ ∅ ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n)
30		breq1 2618	. . . . . . . . . . 11 ⊢ (y = z → (y ≈ k ↔ z ≈ k))
31		raleq1 1783	. . . . . . . . . . 11 ⊢ (y = z → (∀x ∈ y ∃n ∈ ω x ≈ n ↔ ∀x ∈ z ∃n ∈ ω x ≈ n))
32	30, 31	anbi12d 627	. . . . . . . . . 10 ⊢ (y = z → ((y ≈ k ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n)))
33		unieq 2506	. . . . . . . . . . . 12 ⊢ (y = z → ∪y = ∪z)
34	33	breq1d 2625	. . . . . . . . . . 11 ⊢ (y = z → (∪y ≈ n ↔ ∪z ≈ n))
35	34	rexbidv 1661	. . . . . . . . . 10 ⊢ (y = z → (∃n ∈ ω ∪y ≈ n ↔ ∃n ∈ ω ∪z ≈ n))
36	32, 35	imbi12d 625	. . . . . . . . 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 1312	. . . . . . . 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 1809	. . . . . . . . . . . . . . 15 ⊢ k ∈ V
39	38	sucex 3050	. . . . . . . . . . . . . 14 ⊢ suc k ∈ V
40	39	ensym 4410	. . . . . . . . . . . . 13 ⊢ (y ≈ suc k → suc k ≈ y)
41		visset 1809	. . . . . . . . . . . . . 14 ⊢ y ∈ V
42	41	bren 4376	. . . . . . . . . . . . 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		unfi 4546	. . . . . . . . . . . . . . . 16 ⊢ ((∃n ∈ ω ∪(f “ k) ≈ n ⋀ ∃n ∈ ω (f ‘k) ≈ n) → ∃n ∈ ω (∪(f “ k) ∪ (f ‘k)) ≈ n)
45		visset 1809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ f ∈ V
46		imaexg 3414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f ∈ V → (f “ k) ∈ V)
47	45, 46	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f “ k) ∈ V
48		breq1 2618	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z = (f “ k) → (z ≈ k ↔ (f “ k) ≈ k))
49		raleq1 1783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z = (f “ k) → (∀x ∈ z ∃n ∈ ω x ≈ n ↔ ∀x ∈ (f “ k)∃n ∈ ω x ≈ n))
50	48, 49	anbi12d 627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z = (f “ k) → ((z ≈ k ⋀ ∀x ∈ z ∃n ∈ ω x ≈ n) ↔ ((f “ k) ≈ k ⋀ ∀x ∈ (f “ k)∃n ∈ ω x ≈ n)))
51		unieq 2506	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (z = (f “ k) → ∪z = ∪(f “ k))
52	51	breq1d 2625	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z = (f “ k) → (∪z ≈ n ↔ ∪(f “ k) ≈ n))
53	52	rexbidv 1661	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z = (f “ k) → (∃n ∈ ω ∪z ≈ n ↔ ∃n ∈ ω ∪(f “ k) ≈ n))
54	50, 53	imbi12d 625	. . . . . . . . . . . . . . . . . . . 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 1864	. . . . . . . . . . . . . . . . . . 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 3690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:suc k–1-1-onto→y → f:suc k–1-1→y)
58		sssucid 3047	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ k ⊆ suc k
59		f1ores 3705	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f:suc k–1-1→y ⋀ k ⊆ suc k) → (f ↾ k):k–1-1-onto→(f “ k))
60	58, 59	mpan2 695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:suc k–1-1→y → (f ↾ k):k–1-1-onto→(f “ k))
61	38	f1oen 4396	. . . . . . . . . . . . . . . . . . . . . 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 4410	. . . . . . . . . . . . . . . . . . . . 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 389	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f:suc k–1-1-onto→y ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → (f “ k) ≈ k)
66		ssun1 2189	. . . . . . . . . . . . . . . . . . . . . . 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 3692	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (f:suc k–1-1-onto→y → f Fn suc k)
69	38	sucid 3051	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ k ∈ suc k
70		fnsnfv 3769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((f Fn suc k ⋀ k ∈ suc k) → {(f ‘k)} = (f “ {k}))
71	69, 70	mpan2 695	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2180	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:suc k–1-1-onto→y → ((f “ k) ∪ {(f ‘k)}) = ((f “ k) ∪ (f “ {k})))
74		df-suc 2953	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ suc k = (k ∪ {k})
75		imaeq2 3400	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (f “ (k ∪ {k})) = ((f “ k) ∪ (f “ {k}))
78	76, 77	eqtr2 1493	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f “ k) ∪ (f “ {k})) = (f “ suc k)
79	73, 78	syl6eq 1520	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f:suc k–1-1-onto→y → ((f “ k) ∪ {(f ‘k)}) = (f “ suc k))
80		f1ofo 3697	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f:suc k–1-1-onto→y → f:suc k–onto→y)
81		foima 3678	. . . . . . . . . . . . . . . . . . . . . . . 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 1504	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f:suc k–1-1-onto→y → ((f “ k) ∪ {(f ‘k)}) = y)
84	67, 83	sseqtrd 2093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (f:suc k–1-1-onto→y → (f “ k) ⊆ y)
85		ssralv 2110	. . . . . . . . . . . . . . . . . . . . 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 451	. . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . 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 2618	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = (f ‘k) → (x ≈ n ↔ (f ‘k) ≈ n))
92	91	rexbidv 1661	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = (f ‘k) → (∃n ∈ ω x ≈ n ↔ ∃n ∈ ω (f ‘k) ≈ n))
93	92	rcla4va 1871	. . . . . . . . . . . . . . . . . 18 ⊢ (((f ‘k) ∈ y ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω (f ‘k) ≈ n)
94		f1of 3691	. . . . . . . . . . . . . . . . . . 19 ⊢ (f:suc k–1-1-onto→y → f:suc k–→y)
95		ffvelrn 3816	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f:suc k–→y ⋀ k ∈ suc k) → (f ‘k) ∈ y)
96	69, 95	mpan2 695	. . . . . . . . . . . . . . . . . . 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 448	. . . . . . . . . . . . . . . . 17 ⊢ ((f:suc k–1-1-onto→y ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω (f ‘k) ≈ n)
99	98	adantrl 394	. . . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . 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 2508	. . . . . . . . . . . . . . . . . . 19 ⊢ (f:suc k–1-1-onto→y → ∪((f “ k) ∪ {(f ‘k)}) = ∪y)
102		uniun 2515	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪((f “ k) ∪ {(f ‘k)}) = (∪(f “ k) ∪ ∪{(f ‘k)})
103		fvex 3734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f ‘k) ∈ V
104	103	unisn 2513	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪{(f ‘k)} = (f ‘k)
105	104	uneq2i 2177	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪(f “ k) ∪ ∪{(f ‘k)}) = (∪(f “ k) ∪ (f ‘k))
106	102, 105	eqtr2 1493	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪(f “ k) ∪ (f ‘k)) = ∪((f “ k) ∪ {(f ‘k)})
107	101, 106	syl5eq 1516	. . . . . . . . . . . . . . . . . 18 ⊢ (f:suc k–1-1-onto→y → (∪(f “ k) ∪ (f ‘k)) = ∪y)
108	107	breq1d 2625	. . . . . . . . . . . . . . . . 17 ⊢ (f:suc k–1-1-onto→y → ((∪(f “ k) ∪ (f ‘k)) ≈ n ↔ ∪y ≈ n))
109	108	rexbidv 1661	. . . . . . . . . . . . . . . 16 ⊢ (f:suc k–1-1-onto→y → (∃n ∈ ω (∪(f “ k) ∪ (f ‘k)) ≈ n ↔ ∃n ∈ ω ∪y ≈ n))
110	109	adantr 389	. . . . . . . . . . . . . . 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 377	. . . . . . . . . . . . 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 1293	. . . . . . . . . . . 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 1284	. . . . . . . 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 3159	. . . . 5 ⊢ (m ∈ ω → ∀y((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n))
121		relen 4371	. . . . . . . 8 ⊢ Rel ≈
122	121	brrelexi 3208	. . . . . . 7 ⊢ (A ≈ m → A ∈ V)
123		breq1 2618	. . . . . . . . . . 11 ⊢ (y = A → (y ≈ m ↔ A ≈ m))
124		raleq1 1783	. . . . . . . . . . 11 ⊢ (y = A → (∀x ∈ y ∃n ∈ ω x ≈ n ↔ ∀x ∈ A ∃n ∈ ω x ≈ n))
125	123, 124	anbi12d 627	. . . . . . . . . 10 ⊢ (y = A → ((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) ↔ (A ≈ m ⋀ ∀x ∈ A ∃n ∈ ω x ≈ n)))
126		unieq 2506	. . . . . . . . . . . 12 ⊢ (y = A → ∪y = ∪A)
127	126	breq1d 2625	. . . . . . . . . . 11 ⊢ (y = A → (∪y ≈ n ↔ ∪A ≈ n))
128	127	rexbidv 1661	. . . . . . . . . 10 ⊢ (y = A → (∃n ∈ ω ∪y ≈ n ↔ ∃n ∈ ω ∪A ≈ n))
129	125, 128	imbi12d 625	. . . . . . . . 9 ⊢ (y = A → (((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) ↔ ((A ≈ m ⋀ ∀x ∈ A ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪A ≈ n)))
130	129	cla4gv 1858	. . . . . . . 8 ⊢ (A ∈ V → (∀y((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) → ((A ≈ m ⋀ ∀x ∈ A ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪A ≈ n)))
131	130	exp4a 378	. . . . . . 7 ⊢ (A ∈ V → (∀y((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) → (A ≈ m → (∀x ∈ A ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪A ≈ n))))
132	122, 131	syl 10	. . . . . 6 ⊢ (A ≈ m → (∀y((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) → (A ≈ m → (∀x ∈ A ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪A ≈ n))))
133	132	pm2.43b 67	. . . . 5 ⊢ (∀y((y ≈ m ⋀ ∀x ∈ y ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪y ≈ n) → (A ≈ m → (∀x ∈ A ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪A ≈ n)))
134	120, 133	syl 10	. . . 4 ⊢ (m ∈ ω → (A ≈ m → (∀x ∈ A ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪A ≈ n)))
135	134	r19.23aiv 1740	. . 3 ⊢ (∃m ∈ ω A ≈ m → (∀x ∈ A ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪A ≈ n))
136	2, 135	sylbi 199	. 2 ⊢ (∃n ∈ ω A ≈ n → (∀x ∈ A ∃n ∈ ω x ≈ n → ∃n ∈ ω ∪A ≈ n))
137	136	imp 350	1 ⊢ ((∃n ∈ ω A ≈ n ⋀ ∀x ∈ A ∃n ∈ ω x ≈ n) → ∃n ∈ ω ∪A ≈ n)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  ∀wral 1642  ∃wrex 1643  Vcvv 1807   ∪ cun 2041   ⊆ wss 2043  ∅c0 2276  {csn 2405  ∪cuni 2499   class class class wbr 2615  suc csuc 2949  ωcom 3131   ↾ cres 3172   “ cima 3173   Fn wfn 3177  –→wf 3178  –1-1→wf1 3179  –onto→wfo 3180  –1-1-onto→wf1o 3181   ‘cfv 3182   ≈ cen 4365

This theorem is referenced by:  unifi2 4551  iunfi 4561

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2865

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2500  df-int 2530  df-iun 2564  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2829  df-id 2832  df-po 2839  df-so 2849  df-fr 2916  df-we 2933  df-ord 2950  df-on 2951  df-lim 2952  df-suc 2953  df-om 3132  df-xp 3184