Theorem domtriomlem 10437

Description: Lemma for domtriom 10438. (Contributed by Mario Carneiro, 9-Feb-2013.)

Hypotheses

Ref	Expression
domtriomlem.1	⊢ 𝐴 ∈ V
domtriomlem.2	⊢ 𝐵 = {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)}
domtriomlem.3	⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))

Assertion

Ref	Expression
domtriomlem	⊢ (¬ 𝐴 ∈ Fin → ω ≼ 𝐴)

Distinct variable groups:   𝐴,𝑏,𝑛,𝑦   𝐵,𝑏   𝐶,𝑘,𝑛   𝑘,𝑏   𝑦,𝑏

Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑦, 𝑘, 𝑛)   𝐶(𝑦, 𝑏)

Proof of Theorem domtriomlem

Dummy variables 𝑐 𝑚 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		domtriomlem.2	. . . . 5 ⊢ 𝐵 = {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)}
2		domtriomlem.1	. . . . . . 7 ⊢ 𝐴 ∈ V
3	2	pwex 5353	. . . . . 6 ⊢ 𝒫 𝐴 ∈ V
4		simpl 488	. . . . . . . 8 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) → 𝑦 ⊆ 𝐴)
5	4	ss2abi 4021	. . . . . . 7 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦 ∣ 𝑦 ⊆ 𝐴}
6		df-pw 4566	. . . . . . 7 ⊢ 𝒫 𝐴 = {𝑦 ∣ 𝑦 ⊆ 𝐴}
7	5, 6	sseqtrri 3987	. . . . . 6 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
8	3, 7	ssexi 5295	. . . . 5 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ∈ V
9	1, 8	eqeltri 2861	. . . 4 ⊢ 𝐵 ∈ V
10		omex 9615	. . . . 5 ⊢ ω ∈ V
11	10	enref 8984	. . . 4 ⊢ ω ≈ ω
12	9, 11	axcc3 10433	. . 3 ⊢ ∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
13		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑛 ¬ 𝐴 ∈ Fin
14		nfra1 3291	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)
15	13, 14	nfan 1932	. . . . . . 7 ⊢ Ⅎ𝑛(¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
16		nnfi 9155	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → 𝑛 ∈ Fin)
17		pwfi 9281	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
18	16, 17	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19		ficardom 9959	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20		isinf 9228	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚))
21		breq2 5115	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (card‘𝒫 𝑛) → (𝑦 ≈ 𝑚 ↔ 𝑦 ≈ (card‘𝒫 𝑛)))
22	21	anbi2d 642	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (card‘𝒫 𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
23	22	exbidv 1954	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
24	23	rspcv 3579	. . . . . . . . . . . . . 14 ⊢ ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
25	20, 24	syl5 35	. . . . . . . . . . . . 13 ⊢ ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
26	18, 19, 25	3syl 19	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
27		finnum 9946	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28		cardid2 9951	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29		entr 9005	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ≈ (card‘𝒫 𝑛) ∧ (card‘𝒫 𝑛) ≈ 𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)
30	29	expcom 419	. . . . . . . . . . . . . . 15 ⊢ ((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
31	18, 27, 28, 30	4syl 20	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
32	31	anim2d 624	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
33	32	eximdv 1950	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
34	26, 33	syld 48	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
35	1	neeq1i 3024	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36		abn0 4341	. . . . . . . . . . . 12 ⊢ ({𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))
37	35, 36	bitri 278	. . . . . . . . . . 11 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))
38	34, 37	imbitrrdi 255	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅))
39	38	com12 33	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅))
40	39	adantr 486	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅))
41		rsp 3255	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
42	41	adantl 487	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
43	40, 42	mpdd 44	. . . . . . 7 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
44	15, 43	ralrimi 3265	. . . . . 6 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
45	44	3adant2 1149	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
46	45	3expib 1140	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
47	46	eximdv 1950	. . 3 ⊢ (¬ 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
48	12, 47	mpi 21	. 2 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
49		axcc2 10432	. . . . 5 ⊢ ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
50		simp2 1155	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → 𝑐 Fn ω)
51		nfra1 3291	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵
52		nfra1 3291	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))
53	51, 52	nfan 1932	. . . . . . . . . 10 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
54		fvex 6898	. . . . . . . . . . . . . . . 16 ⊢ (𝑏‘𝑛) ∈ V
55		sseq1 3963	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ⊆ 𝐴 ↔ (𝑏‘𝑛) ⊆ 𝐴))
56		breq1 5114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏‘𝑛) ≈ 𝒫 𝑛))
57	55, 56	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑏‘𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛)))
58	54, 57, 1	elab2 3643	. . . . . . . . . . . . . . 15 ⊢ ((𝑏‘𝑛) ∈ 𝐵 ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛))
59	58	simprbi 503	. . . . . . . . . . . . . 14 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ≈ 𝒫 𝑛)
60	59	ralimi 3104	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛)
61		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (𝑏‘𝑛) = (𝑏‘𝑘))
62		pweq 4578	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
63	61, 62	breq12d 5124	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ (𝑏‘𝑘) ≈ 𝒫 𝑘))
64	63	cbvralvw 3245	. . . . . . . . . . . . . . 15 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘)
65		peano2 7888	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66		omelon 9618	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
67	66	onelssi 6481	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68		ssralv 4007	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
69	65, 67, 68	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
70		pwsdompw 10198	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))
71	70	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
72	69, 71	syld 48	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
73		sdomdif 9116	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛) → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)
74	72, 73	syl6 36	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
75	64, 74	biimtrid 245	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
76	54	difexi 5303	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V
77		domtriomlem.3	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
78	77	fvmpt2 7005	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ω ∧ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V) → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
79	76, 78	mpan2 704	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
80	79	neeq1d 3019	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ ↔ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
81	75, 80	sylibrd 262	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → (𝐶‘𝑛) ≠ ∅))
82	60, 81	syl5com 32	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
83	82	adantr 486	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
84		rsp 3255	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
85	84	adantl 487	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
86	83, 85	mpdd 44	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
87	53, 86	ralrimi 3265	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
88	87	3adant2 1149	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
89	50, 88	jca 521	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
90	89	3expib 1140	. . . . . 6 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
91	90	eximdv 1950	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
92	49, 91	mpi 21	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
93		simp2 1155	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐 Fn ω)
94		nfra1 3291	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)
95	51, 94	nfan 1932	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
96		rsp 3255	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
97	96	com12 33	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
98		rsp 3255	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
99	98	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ∈ 𝐵))
100	79	eleq2d 2851	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
101		eldifi 4085	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ (𝑏‘𝑛))
102	100, 101	biimtrdi 256	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑛)))
103	58	simplbi 502	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ⊆ 𝐴)
104	103	sseld 3937	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ 𝐴))
105	102, 104	syl9 78	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴)))
106	99, 105	syld 48	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴)))
107	106	com23 87	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴)))
108	97, 107	syld 48	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴)))
109	108	com13 89	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴)))
110	109	imp 412	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴))
111	95, 110	ralrimi 3265	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
112	111	3adant2 1149	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
113		ffnfv 7118	. . . . . . . . . 10 ⊢ (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴))
114	93, 112, 113	sylanbrc 595	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω⟶𝐴)
115		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑘 ∈ ω
116		nnord 7872	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ω → Ord 𝑘)
117		nnord 7872	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → Ord 𝑛)
118		ordtri3or 6397	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
119	116, 117, 118	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
120		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝑐‘𝑛) = (𝑐‘𝑘))
121		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗))
122	121	cbviunv 5005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗)
123		iuneq1 4975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
124	122, 123	eqtrid 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
125	61, 124	difeq12d 4082	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) = ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
126	120, 125	eleq12d 2859	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ↔ (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
127	126	rspccv 3580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑘 ∈ ω → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
128	96, 100	mpbidi 244	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
129	94, 128	ralrimi 3265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
130	127, 129	syl11 34	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
131	130	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
132		eldifi 4085	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑘) ∈ (𝑏‘𝑘))
133		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ (𝑏‘𝑘) ↔ (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
134	132, 133	imbitrid 247	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
135	134	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
136	131, 135	syld 48	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
137	136	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))
138		ssiun2 5014	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑛 → (𝑏‘𝑘) ⊆ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
139	138	sseld 3937	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝑛 → ((𝑐‘𝑛) ∈ (𝑏‘𝑘) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
140	137, 139	syl5 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
141	140	3impib 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
142	128	com12 33	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
143	142	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
144	143	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
145	144	eldifbd 3919	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
146	145	3adant1 1148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
147	141, 146	pm2.21dd 198	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
148	147	3exp 1137	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
149		2a1 29	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
150		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 𝑛 → (𝑏‘𝑗) = (𝑏‘𝑛))
151	150	ssiun2s 5015	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝑘 → (𝑏‘𝑛) ⊆ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
152	151	sseld 3937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
153	101, 152	syl5 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
154	144, 153	syl5 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
155	154	3impib 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
156		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
157		eldifn 4086	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
158	156, 157	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
159	158	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
160	131, 159	syld 48	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
162	161	3imp 1128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
163	155, 162	pm2.21dd 198	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
164	163	3exp 1137	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
165	148, 149, 164	3jaoi 1454	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
166	165	com12 33	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
167	166	3expia 1139	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))))
168	119, 167	mpid 45	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
169	168	com3r 88	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
170	169	expd 421	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))))
171	94, 115, 170	ralrimd 3272	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
172	171	ralrimiv 3158	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
173	172	3ad2ant3 1153	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
174		dff13 7254	. . . . . . . . 9 ⊢ (𝑐:ω–1-1→𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
175	114, 173, 174	sylanbrc 595	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω–1-1→𝐴)
176	175	19.8ad 2221	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∃𝑐 𝑐:ω–1-1→𝐴)
177	2	brdom 8959	. . . . . . 7 ⊢ (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1→𝐴)
178	176, 177	sylibr 237	. . . . . 6 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)
179	178	3expib 1140	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
180	179	exlimdv 1966	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
181	92, 180	mpd 16	. . 3 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
182	181	exlimiv 1963	. 2 ⊢ (∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
183	48, 182	syl 18	1 ⊢ (¬ 𝐴 ∈ Fin → ω ≼ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146  {cab 2743   ≠ wne 2960  ∀wral 3081  Vcvv 3457   ∖ cdif 3903   ⊆ wss 3906  ∅c0 4286  𝒫 cpw 4564  ∪ ciun 4958   class class class wbr 5111   ↦ cmpt 5194  dom cdm 5663  Ord word 6363  suc csuc 6366   Fn wfn 6535  ⟶wf 6536  –1-1→wf1 6537  ‘cfv 6540  ωcom 7864   ≈ cen 8942   ≼ cdom 8943   ≺ csdm 8944  Fincfn 8945  cardccrd 9933

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-inf2 9613  ax-cc 10430

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-oadd 8459  df-er 8696  df-map 8828  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-dju 9899  df-card 9937

This theorem is used by:  domtriom  10438