Theorem domtriomlem 10182

Description: Lemma for domtriom 10183. (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 5306	. . . . . 6 ⊢ 𝒫 𝐴 ∈ V
4		simpl 482	. . . . . . . 8 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) → 𝑦 ⊆ 𝐴)
5	4	ss2abi 4004	. . . . . . 7 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦 ∣ 𝑦 ⊆ 𝐴}
6		df-pw 4540	. . . . . . 7 ⊢ 𝒫 𝐴 = {𝑦 ∣ 𝑦 ⊆ 𝐴}
7	5, 6	sseqtrri 3962	. . . . . 6 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
8	3, 7	ssexi 5249	. . . . 5 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ∈ V
9	1, 8	eqeltri 2836	. . . 4 ⊢ 𝐵 ∈ V
10		omex 9362	. . . . 5 ⊢ ω ∈ V
11	10	enref 8744	. . . 4 ⊢ ω ≈ ω
12	9, 11	axcc3 10178	. . 3 ⊢ ∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
13		nfv 1920	. . . . . . . 8 ⊢ Ⅎ𝑛 ¬ 𝐴 ∈ Fin
14		nfra1 3144	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)
15	13, 14	nfan 1905	. . . . . . 7 ⊢ Ⅎ𝑛(¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
16		nnfi 8915	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → 𝑛 ∈ Fin)
17		pwfi 8926	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
18	16, 17	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19		ficardom 9703	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20		isinf 8997	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚))
21		breq2 5082	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (card‘𝒫 𝑛) → (𝑦 ≈ 𝑚 ↔ 𝑦 ≈ (card‘𝒫 𝑛)))
22	21	anbi2d 628	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (card‘𝒫 𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
23	22	exbidv 1927	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
24	23	rspcv 3555	. . . . . . . . . . . . . 14 ⊢ ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
25	20, 24	syl5 34	. . . . . . . . . . . . 13 ⊢ ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
26	18, 19, 25	3syl 18	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
27		finnum 9690	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28		cardid2 9695	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29		entr 8763	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ≈ (card‘𝒫 𝑛) ∧ (card‘𝒫 𝑛) ≈ 𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)
30	29	expcom 413	. . . . . . . . . . . . . . 15 ⊢ ((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
31	18, 27, 28, 30	4syl 19	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
32	31	anim2d 611	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
33	32	eximdv 1923	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
34	26, 33	syld 47	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
35	1	neeq1i 3009	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36		abn0 4319	. . . . . . . . . . . 12 ⊢ ({𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))
37	35, 36	bitri 274	. . . . . . . . . . 11 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))
38	34, 37	syl6ibr 251	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅))
39	38	com12 32	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅))
40	39	adantr 480	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅))
41		rsp 3131	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
42	41	adantl 481	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
43	40, 42	mpdd 43	. . . . . . 7 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
44	15, 43	ralrimi 3141	. . . . . 6 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
45	44	3adant2 1129	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
46	45	3expib 1120	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
47	46	eximdv 1923	. . 3 ⊢ (¬ 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
48	12, 47	mpi 20	. 2 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
49		axcc2 10177	. . . . 5 ⊢ ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
50		simp2 1135	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → 𝑐 Fn ω)
51		nfra1 3144	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵
52		nfra1 3144	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))
53	51, 52	nfan 1905	. . . . . . . . . 10 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
54		fvex 6781	. . . . . . . . . . . . . . . 16 ⊢ (𝑏‘𝑛) ∈ V
55		sseq1 3950	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ⊆ 𝐴 ↔ (𝑏‘𝑛) ⊆ 𝐴))
56		breq1 5081	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏‘𝑛) ≈ 𝒫 𝑛))
57	55, 56	anbi12d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑏‘𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛)))
58	54, 57, 1	elab2 3614	. . . . . . . . . . . . . . 15 ⊢ ((𝑏‘𝑛) ∈ 𝐵 ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛))
59	58	simprbi 496	. . . . . . . . . . . . . 14 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ≈ 𝒫 𝑛)
60	59	ralimi 3088	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛)
61		fveq2 6768	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (𝑏‘𝑛) = (𝑏‘𝑘))
62		pweq 4554	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
63	61, 62	breq12d 5091	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ (𝑏‘𝑘) ≈ 𝒫 𝑘))
64	63	cbvralvw 3380	. . . . . . . . . . . . . . 15 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘)
65		peano2 7724	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66		omelon 9365	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
67	66	onelssi 6372	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68		ssralv 3991	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
69	65, 67, 68	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
70		pwsdompw 9944	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))
71	70	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
72	69, 71	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
73		sdomdif 8877	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛) → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)
74	72, 73	syl6 35	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
75	64, 74	syl5bi 241	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
76	54	difexi 5255	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V
77		domtriomlem.3	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
78	77	fvmpt2 6880	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ω ∧ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V) → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
79	76, 78	mpan2 687	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
80	79	neeq1d 3004	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ ↔ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
81	75, 80	sylibrd 258	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → (𝐶‘𝑛) ≠ ∅))
82	60, 81	syl5com 31	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
83	82	adantr 480	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
84		rsp 3131	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
85	84	adantl 481	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
86	83, 85	mpdd 43	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
87	53, 86	ralrimi 3141	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
88	87	3adant2 1129	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
89	50, 88	jca 511	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
90	89	3expib 1120	. . . . . 6 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
91	90	eximdv 1923	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
92	49, 91	mpi 20	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
93		simp2 1135	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐 Fn ω)
94		nfra1 3144	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)
95	51, 94	nfan 1905	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
96		rsp 3131	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
97	96	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
98		rsp 3131	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
99	98	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ∈ 𝐵))
100	79	eleq2d 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
101		eldifi 4065	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ (𝑏‘𝑛))
102	100, 101	syl6bi 252	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑛)))
103	58	simplbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ⊆ 𝐴)
104	103	sseld 3924	. . . . . . . . . . . . . . . . . 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 3141	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
112	111	3adant2 1129	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
113		ffnfv 6986	. . . . . . . . . 10 ⊢ (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴))
114	93, 112, 113	sylanbrc 582	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω⟶𝐴)
115		nfv 1920	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑘 ∈ ω
116		nnord 7708	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ω → Ord 𝑘)
117		nnord 7708	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → Ord 𝑛)
118		ordtri3or 6295	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
119	116, 117, 118	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
120		fveq2 6768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝑐‘𝑛) = (𝑐‘𝑘))
121		fveq2 6768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗))
122	121	cbviunv 4974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗)
123		iuneq1 4945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
124	122, 123	eqtrid 2791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
125	61, 124	difeq12d 4062	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) = ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
126	120, 125	eleq12d 2834	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ↔ (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
127	126	rspccv 3557	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑘 ∈ ω → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
128	96, 100	mpbidi 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
129	94, 128	ralrimi 3141	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
130	127, 129	syl11 33	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
131	130	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
132		eldifi 4065	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑘) ∈ (𝑏‘𝑘))
133		eleq1 2827	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ (𝑏‘𝑘) ↔ (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
134	132, 133	syl5ib 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
135	134	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
136	131, 135	syld 47	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
137	136	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))
138		ssiun2 4981	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑛 → (𝑏‘𝑘) ⊆ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
139	138	sseld 3924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝑛 → ((𝑐‘𝑛) ∈ (𝑏‘𝑘) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
140	137, 139	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
141	140	3impib 1114	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
142	128	com12 32	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
143	142	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
144	143	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
145	144	eldifbd 3904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
146	145	3adant1 1128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
147	141, 146	pm2.21dd 194	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
148	147	3exp 1117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
149		2a1 28	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
150		fveq2 6768	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 𝑛 → (𝑏‘𝑗) = (𝑏‘𝑛))
151	150	ssiun2s 4982	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝑘 → (𝑏‘𝑛) ⊆ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
152	151	sseld 3924	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
153	101, 152	syl5 34	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
154	144, 153	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
155	154	3impib 1114	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
156		eleq1 2827	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
157		eldifn 4066	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
158	156, 157	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
159	158	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
160	131, 159	syld 47	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
162	161	3imp 1109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
163	155, 162	pm2.21dd 194	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
164	163	3exp 1117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
165	148, 149, 164	3jaoi 1425	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
166	165	com12 32	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
167	166	3expia 1119	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))))
168	119, 167	mpid 44	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
169	168	com3r 87	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
170	169	expd 415	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))))
171	94, 115, 170	ralrimd 3143	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
172	171	ralrimiv 3108	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
173	172	3ad2ant3 1133	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
174		dff13 7122	. . . . . . . . 9 ⊢ (𝑐:ω–1-1→𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
175	114, 173, 174	sylanbrc 582	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω–1-1→𝐴)
176	175	19.8ad 2178	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∃𝑐 𝑐:ω–1-1→𝐴)
177	2	brdom 8721	. . . . . . 7 ⊢ (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1→𝐴)
178	176, 177	sylibr 233	. . . . . 6 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)
179	178	3expib 1120	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
180	179	exlimdv 1939	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
181	92, 180	mpd 15	. . 3 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
182	181	exlimiv 1936	. 2 ⊢ (∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
183	48, 182	syl 17	1 ⊢ (¬ 𝐴 ∈ Fin → ω ≼ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ w3o 1084   ∧ w3a 1085   = wceq 1541  ∃wex 1785   ∈ wcel 2109  {cab 2716   ≠ wne 2944  ∀wral 3065  Vcvv 3430   ∖ cdif 3888   ⊆ wss 3891  ∅c0 4261  𝒫 cpw 4538  ∪ ciun 4929   class class class wbr 5078   ↦ cmpt 5161  dom cdm 5588  Ord word 6262  suc csuc 6265   Fn wfn 6425  ⟶wf 6426  –1-1→wf1 6427  ‘cfv 6430  ωcom 7700   ≈ cen 8704   ≼ cdom 8705   ≺ csdm 8706  Fincfn 8707  cardccrd 9677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-inf2 9360  ax-cc 10175

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rmo 3073  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-int 4885  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-oprab 7272  df-mpo 7273  df-om 7701  df-1st 7817  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-1o 8281  df-2o 8282  df-oadd 8285  df-er 8472  df-map 8591  df-en 8708  df-dom 8709  df-sdom 8710  df-fin 8711  df-dju 9643  df-card 9681

This theorem is referenced by:  domtriom  10183