Theorem domtriomlem 10344

Description: Lemma for domtriom 10345. (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 5322	. . . . . 6 ⊢ 𝒫 𝐴 ∈ V
4		simpl 482	. . . . . . . 8 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) → 𝑦 ⊆ 𝐴)
5	4	ss2abi 4015	. . . . . . 7 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦 ∣ 𝑦 ⊆ 𝐴}
6		df-pw 4553	. . . . . . 7 ⊢ 𝒫 𝐴 = {𝑦 ∣ 𝑦 ⊆ 𝐴}
7	5, 6	sseqtrri 3980	. . . . . 6 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
8	3, 7	ssexi 5264	. . . . 5 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ∈ V
9	1, 8	eqeltri 2829	. . . 4 ⊢ 𝐵 ∈ V
10		omex 9544	. . . . 5 ⊢ ω ∈ V
11	10	enref 8918	. . . 4 ⊢ ω ≈ ω
12	9, 11	axcc3 10340	. . 3 ⊢ ∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
13		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑛 ¬ 𝐴 ∈ Fin
14		nfra1 3257	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)
15	13, 14	nfan 1900	. . . . . . 7 ⊢ Ⅎ𝑛(¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
16		nnfi 9088	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → 𝑛 ∈ Fin)
17		pwfi 9214	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
18	16, 17	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19		ficardom 9865	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20		isinf 9160	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚))
21		breq2 5099	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (card‘𝒫 𝑛) → (𝑦 ≈ 𝑚 ↔ 𝑦 ≈ (card‘𝒫 𝑛)))
22	21	anbi2d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (card‘𝒫 𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
23	22	exbidv 1922	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
24	23	rspcv 3569	. . . . . . . . . . . . . 14 ⊢ ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
25	20, 24	syl5 34	. . . . . . . . . . . . 13 ⊢ ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
26	18, 19, 25	3syl 18	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
27		finnum 9852	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28		cardid2 9857	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29		entr 8939	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ≈ (card‘𝒫 𝑛) ∧ (card‘𝒫 𝑛) ≈ 𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)
30	29	expcom 413	. . . . . . . . . . . . . . 15 ⊢ ((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
31	18, 27, 28, 30	4syl 19	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
32	31	anim2d 612	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
33	32	eximdv 1918	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
34	26, 33	syld 47	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
35	1	neeq1i 2993	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36		abn0 4334	. . . . . . . . . . . 12 ⊢ ({𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))
37	35, 36	bitri 275	. . . . . . . . . . 11 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))
38	34, 37	imbitrrdi 252	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅))
39	38	com12 32	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅))
40	39	adantr 480	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅))
41		rsp 3221	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
42	41	adantl 481	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
43	40, 42	mpdd 43	. . . . . . 7 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
44	15, 43	ralrimi 3231	. . . . . 6 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
45	44	3adant2 1131	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
46	45	3expib 1122	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
47	46	eximdv 1918	. . 3 ⊢ (¬ 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
48	12, 47	mpi 20	. 2 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
49		axcc2 10339	. . . . 5 ⊢ ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
50		simp2 1137	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → 𝑐 Fn ω)
51		nfra1 3257	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵
52		nfra1 3257	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))
53	51, 52	nfan 1900	. . . . . . . . . 10 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
54		fvex 6844	. . . . . . . . . . . . . . . 16 ⊢ (𝑏‘𝑛) ∈ V
55		sseq1 3956	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ⊆ 𝐴 ↔ (𝑏‘𝑛) ⊆ 𝐴))
56		breq1 5098	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏‘𝑛) ≈ 𝒫 𝑛))
57	55, 56	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑏‘𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛)))
58	54, 57, 1	elab2 3634	. . . . . . . . . . . . . . 15 ⊢ ((𝑏‘𝑛) ∈ 𝐵 ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛))
59	58	simprbi 496	. . . . . . . . . . . . . 14 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ≈ 𝒫 𝑛)
60	59	ralimi 3070	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛)
61		fveq2 6831	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (𝑏‘𝑛) = (𝑏‘𝑘))
62		pweq 4565	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
63	61, 62	breq12d 5108	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ (𝑏‘𝑘) ≈ 𝒫 𝑘))
64	63	cbvralvw 3211	. . . . . . . . . . . . . . 15 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘)
65		peano2 7829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66		omelon 9547	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
67	66	onelssi 6430	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68		ssralv 3999	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
69	65, 67, 68	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
70		pwsdompw 10105	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))
71	70	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
72	69, 71	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
73		sdomdif 9049	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛) → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)
74	72, 73	syl6 35	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
75	64, 74	biimtrid 242	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
76	54	difexi 5272	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V
77		domtriomlem.3	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
78	77	fvmpt2 6949	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ω ∧ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V) → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
79	76, 78	mpan2 691	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
80	79	neeq1d 2988	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ ↔ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
81	75, 80	sylibrd 259	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → (𝐶‘𝑛) ≠ ∅))
82	60, 81	syl5com 31	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
83	82	adantr 480	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
84		rsp 3221	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
85	84	adantl 481	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
86	83, 85	mpdd 43	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
87	53, 86	ralrimi 3231	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
88	87	3adant2 1131	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
89	50, 88	jca 511	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
90	89	3expib 1122	. . . . . 6 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
91	90	eximdv 1918	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
92	49, 91	mpi 20	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
93		simp2 1137	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐 Fn ω)
94		nfra1 3257	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)
95	51, 94	nfan 1900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
96		rsp 3221	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
97	96	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
98		rsp 3221	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
99	98	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ∈ 𝐵))
100	79	eleq2d 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
101		eldifi 4080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ (𝑏‘𝑛))
102	100, 101	biimtrdi 253	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑛)))
103	58	simplbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ⊆ 𝐴)
104	103	sseld 3929	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ 𝐴))
105	102, 104	syl9 77	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴)))
106	99, 105	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴)))
107	106	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴)))
108	97, 107	syld 47	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴)))
109	108	com13 88	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴)))
110	109	imp 406	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴))
111	95, 110	ralrimi 3231	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
112	111	3adant2 1131	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
113		ffnfv 7061	. . . . . . . . . 10 ⊢ (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴))
114	93, 112, 113	sylanbrc 583	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω⟶𝐴)
115		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑘 ∈ ω
116		nnord 7813	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ω → Ord 𝑘)
117		nnord 7813	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → Ord 𝑛)
118		ordtri3or 6346	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
119	116, 117, 118	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
120		fveq2 6831	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝑐‘𝑛) = (𝑐‘𝑘))
121		fveq2 6831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗))
122	121	cbviunv 4991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗)
123		iuneq1 4960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
124	122, 123	eqtrid 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
125	61, 124	difeq12d 4076	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) = ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
126	120, 125	eleq12d 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ↔ (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
127	126	rspccv 3570	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑘 ∈ ω → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
128	96, 100	mpbidi 241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
129	94, 128	ralrimi 3231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
130	127, 129	syl11 33	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
131	130	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
132		eldifi 4080	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑘) ∈ (𝑏‘𝑘))
133		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ (𝑏‘𝑘) ↔ (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
134	132, 133	imbitrid 244	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
135	134	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
136	131, 135	syld 47	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
137	136	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))
138		ssiun2 5000	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑛 → (𝑏‘𝑘) ⊆ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
139	138	sseld 3929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝑛 → ((𝑐‘𝑛) ∈ (𝑏‘𝑘) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
140	137, 139	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
141	140	3impib 1116	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
142	128	com12 32	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
143	142	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
144	143	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
145	144	eldifbd 3911	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
146	145	3adant1 1130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
147	141, 146	pm2.21dd 195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
148	147	3exp 1119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
149		2a1 28	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
150		fveq2 6831	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 𝑛 → (𝑏‘𝑗) = (𝑏‘𝑛))
151	150	ssiun2s 5001	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝑘 → (𝑏‘𝑛) ⊆ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
152	151	sseld 3929	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
153	101, 152	syl5 34	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
154	144, 153	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
155	154	3impib 1116	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
156		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
157		eldifn 4081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
158	156, 157	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
159	158	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
160	131, 159	syld 47	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
162	161	3imp 1110	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
163	155, 162	pm2.21dd 195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
164	163	3exp 1119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
165	148, 149, 164	3jaoi 1430	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
166	165	com12 32	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
167	166	3expia 1121	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))))
168	119, 167	mpid 44	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
169	168	com3r 87	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
170	169	expd 415	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))))
171	94, 115, 170	ralrimd 3238	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
172	171	ralrimiv 3124	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
173	172	3ad2ant3 1135	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
174		dff13 7197	. . . . . . . . 9 ⊢ (𝑐:ω–1-1→𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
175	114, 173, 174	sylanbrc 583	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω–1-1→𝐴)
176	175	19.8ad 2187	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∃𝑐 𝑐:ω–1-1→𝐴)
177	2	brdom 8893	. . . . . . 7 ⊢ (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1→𝐴)
178	176, 177	sylibr 234	. . . . . 6 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)
179	178	3expib 1122	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
180	179	exlimdv 1934	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
181	92, 180	mpd 15	. . 3 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
182	181	exlimiv 1931	. 2 ⊢ (∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
183	48, 182	syl 17	1 ⊢ (¬ 𝐴 ∈ Fin → ω ≼ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ w3o 1085   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113  {cab 2711   ≠ wne 2929  ∀wral 3048  Vcvv 3437   ∖ cdif 3895   ⊆ wss 3898  ∅c0 4282  𝒫 cpw 4551  ∪ ciun 4943   class class class wbr 5095   ↦ cmpt 5176  dom cdm 5621  Ord word 6313  suc csuc 6316   Fn wfn 6484  ⟶wf 6485  –1-1→wf1 6486  ‘cfv 6489  ωcom 7805   ≈ cen 8876   ≼ cdom 8877   ≺ csdm 8878  Fincfn 8879  cardccrd 9839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-inf2 9542  ax-cc 10337

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-int 4900  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-om 7806  df-1st 7930  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-1o 8394  df-2o 8395  df-oadd 8398  df-er 8631  df-map 8761  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-dju 9805  df-card 9843

This theorem is referenced by:  domtriom  10345