Theorem domtriomlem 10482

Description: Lemma for domtriom 10483. (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 5380	. . . . . 6 ⊢ 𝒫 𝐴 ∈ V
4		simpl 482	. . . . . . . 8 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) → 𝑦 ⊆ 𝐴)
5	4	ss2abi 4067	. . . . . . 7 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦 ∣ 𝑦 ⊆ 𝐴}
6		df-pw 4602	. . . . . . 7 ⊢ 𝒫 𝐴 = {𝑦 ∣ 𝑦 ⊆ 𝐴}
7	5, 6	sseqtrri 4033	. . . . . 6 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
8	3, 7	ssexi 5322	. . . . 5 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ∈ V
9	1, 8	eqeltri 2837	. . . 4 ⊢ 𝐵 ∈ V
10		omex 9683	. . . . 5 ⊢ ω ∈ V
11	10	enref 9025	. . . 4 ⊢ ω ≈ ω
12	9, 11	axcc3 10478	. . 3 ⊢ ∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
13		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑛 ¬ 𝐴 ∈ Fin
14		nfra1 3284	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)
15	13, 14	nfan 1899	. . . . . . 7 ⊢ Ⅎ𝑛(¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
16		nnfi 9207	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → 𝑛 ∈ Fin)
17		pwfi 9357	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
18	16, 17	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19		ficardom 10001	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20		isinf 9296	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚))
21		breq2 5147	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (card‘𝒫 𝑛) → (𝑦 ≈ 𝑚 ↔ 𝑦 ≈ (card‘𝒫 𝑛)))
22	21	anbi2d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (card‘𝒫 𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
23	22	exbidv 1921	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
24	23	rspcv 3618	. . . . . . . . . . . . . 14 ⊢ ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
25	20, 24	syl5 34	. . . . . . . . . . . . 13 ⊢ ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
26	18, 19, 25	3syl 18	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
27		finnum 9988	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28		cardid2 9993	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29		entr 9046	. . . . . . . . . . . . . . . 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 1917	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
34	26, 33	syld 47	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
35	1	neeq1i 3005	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36		abn0 4385	. . . . . . . . . . . 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 3247	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
42	41	adantl 481	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
43	40, 42	mpdd 43	. . . . . . 7 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
44	15, 43	ralrimi 3257	. . . . . 6 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
45	44	3adant2 1132	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
46	45	3expib 1123	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
47	46	eximdv 1917	. . 3 ⊢ (¬ 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
48	12, 47	mpi 20	. 2 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
49		axcc2 10477	. . . . 5 ⊢ ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
50		simp2 1138	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → 𝑐 Fn ω)
51		nfra1 3284	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵
52		nfra1 3284	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))
53	51, 52	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
54		fvex 6919	. . . . . . . . . . . . . . . 16 ⊢ (𝑏‘𝑛) ∈ V
55		sseq1 4009	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ⊆ 𝐴 ↔ (𝑏‘𝑛) ⊆ 𝐴))
56		breq1 5146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏‘𝑛) ≈ 𝒫 𝑛))
57	55, 56	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑏‘𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛)))
58	54, 57, 1	elab2 3682	. . . . . . . . . . . . . . 15 ⊢ ((𝑏‘𝑛) ∈ 𝐵 ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛))
59	58	simprbi 496	. . . . . . . . . . . . . 14 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ≈ 𝒫 𝑛)
60	59	ralimi 3083	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛)
61		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (𝑏‘𝑛) = (𝑏‘𝑘))
62		pweq 4614	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
63	61, 62	breq12d 5156	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ (𝑏‘𝑘) ≈ 𝒫 𝑘))
64	63	cbvralvw 3237	. . . . . . . . . . . . . . 15 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘)
65		peano2 7912	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66		omelon 9686	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
67	66	onelssi 6499	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68		ssralv 4052	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
69	65, 67, 68	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
70		pwsdompw 10243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))
71	70	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
72	69, 71	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
73		sdomdif 9165	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛) → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)
74	72, 73	syl6 35	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
75	64, 74	biimtrid 242	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
76	54	difexi 5330	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V
77		domtriomlem.3	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
78	77	fvmpt2 7027	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ω ∧ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V) → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
79	76, 78	mpan2 691	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
80	79	neeq1d 3000	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ ↔ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
81	75, 80	sylibrd 259	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → (𝐶‘𝑛) ≠ ∅))
82	60, 81	syl5com 31	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
83	82	adantr 480	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
84		rsp 3247	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
85	84	adantl 481	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
86	83, 85	mpdd 43	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
87	53, 86	ralrimi 3257	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
88	87	3adant2 1132	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
89	50, 88	jca 511	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
90	89	3expib 1123	. . . . . 6 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
91	90	eximdv 1917	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
92	49, 91	mpi 20	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
93		simp2 1138	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐 Fn ω)
94		nfra1 3284	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)
95	51, 94	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
96		rsp 3247	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
97	96	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
98		rsp 3247	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
99	98	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ∈ 𝐵))
100	79	eleq2d 2827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
101		eldifi 4131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ (𝑏‘𝑛))
102	100, 101	biimtrdi 253	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑛)))
103	58	simplbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ⊆ 𝐴)
104	103	sseld 3982	. . . . . . . . . . . . . . . . . 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 3257	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
112	111	3adant2 1132	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
113		ffnfv 7139	. . . . . . . . . 10 ⊢ (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴))
114	93, 112, 113	sylanbrc 583	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω⟶𝐴)
115		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑘 ∈ ω
116		nnord 7895	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ω → Ord 𝑘)
117		nnord 7895	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → Ord 𝑛)
118		ordtri3or 6416	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
119	116, 117, 118	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
120		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝑐‘𝑛) = (𝑐‘𝑘))
121		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗))
122	121	cbviunv 5040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗)
123		iuneq1 5008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
124	122, 123	eqtrid 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
125	61, 124	difeq12d 4127	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) = ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
126	120, 125	eleq12d 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ↔ (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
127	126	rspccv 3619	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑘 ∈ ω → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
128	96, 100	mpbidi 241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
129	94, 128	ralrimi 3257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
130	127, 129	syl11 33	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
131	130	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
132		eldifi 4131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑘) ∈ (𝑏‘𝑘))
133		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ (𝑏‘𝑘) ↔ (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
134	132, 133	imbitrid 244	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
135	134	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
136	131, 135	syld 47	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
137	136	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))
138		ssiun2 5047	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑛 → (𝑏‘𝑘) ⊆ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
139	138	sseld 3982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝑛 → ((𝑐‘𝑛) ∈ (𝑏‘𝑘) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
140	137, 139	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
141	140	3impib 1117	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
142	128	com12 32	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
143	142	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
144	143	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
145	144	eldifbd 3964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
146	145	3adant1 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
147	141, 146	pm2.21dd 195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
148	147	3exp 1120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
149		2a1 28	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
150		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 𝑛 → (𝑏‘𝑗) = (𝑏‘𝑛))
151	150	ssiun2s 5048	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝑘 → (𝑏‘𝑛) ⊆ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
152	151	sseld 3982	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
153	101, 152	syl5 34	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
154	144, 153	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
155	154	3impib 1117	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
156		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
157		eldifn 4132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
158	156, 157	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
159	158	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
160	131, 159	syld 47	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
162	161	3imp 1111	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
163	155, 162	pm2.21dd 195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
164	163	3exp 1120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
165	148, 149, 164	3jaoi 1430	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
166	165	com12 32	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
167	166	3expia 1122	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))))
168	119, 167	mpid 44	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
169	168	com3r 87	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
170	169	expd 415	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))))
171	94, 115, 170	ralrimd 3264	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
172	171	ralrimiv 3145	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
173	172	3ad2ant3 1136	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
174		dff13 7275	. . . . . . . . 9 ⊢ (𝑐:ω–1-1→𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
175	114, 173, 174	sylanbrc 583	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω–1-1→𝐴)
176	175	19.8ad 2182	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∃𝑐 𝑐:ω–1-1→𝐴)
177	2	brdom 9001	. . . . . . 7 ⊢ (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1→𝐴)
178	176, 177	sylibr 234	. . . . . 6 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)
179	178	3expib 1123	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
180	179	exlimdv 1933	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
181	92, 180	mpd 15	. . 3 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
182	181	exlimiv 1930	. 2 ⊢ (∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
183	48, 182	syl 17	1 ⊢ (¬ 𝐴 ∈ Fin → ω ≼ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ w3o 1086   ∧ w3a 1087   = wceq 1540  ∃wex 1779   ∈ wcel 2108  {cab 2714   ≠ wne 2940  ∀wral 3061  Vcvv 3480   ∖ cdif 3948   ⊆ wss 3951  ∅c0 4333  𝒫 cpw 4600  ∪ ciun 4991   class class class wbr 5143   ↦ cmpt 5225  dom cdm 5685  Ord word 6383  suc csuc 6386   Fn wfn 6556  ⟶wf 6557  –1-1→wf1 6558  ‘cfv 6561  ωcom 7887   ≈ cen 8982   ≼ cdom 8983   ≺ csdm 8984  Fincfn 8985  cardccrd 9975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cc 10475

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-dju 9941  df-card 9979

This theorem is referenced by:  domtriom  10483