Theorem domtriomlem 10378

Description: Lemma for domtriom 10379. (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 5335	. . . . . 6 ⊢ 𝒫 𝐴 ∈ V
4		simpl 483	. . . . . . . 8 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) → 𝑦 ⊆ 𝐴)
5	4	ss2abi 4023	. . . . . . 7 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦 ∣ 𝑦 ⊆ 𝐴}
6		df-pw 4562	. . . . . . 7 ⊢ 𝒫 𝐴 = {𝑦 ∣ 𝑦 ⊆ 𝐴}
7	5, 6	sseqtrri 3981	. . . . . 6 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴
8	3, 7	ssexi 5279	. . . . 5 ⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ∈ V
9	1, 8	eqeltri 2834	. . . 4 ⊢ 𝐵 ∈ V
10		omex 9579	. . . . 5 ⊢ ω ∈ V
11	10	enref 8925	. . . 4 ⊢ ω ≈ ω
12	9, 11	axcc3 10374	. . 3 ⊢ ∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
13		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑛 ¬ 𝐴 ∈ Fin
14		nfra1 3267	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)
15	13, 14	nfan 1902	. . . . . . 7 ⊢ Ⅎ𝑛(¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))
16		nnfi 9111	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → 𝑛 ∈ Fin)
17		pwfi 9122	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Fin ↔ 𝒫 𝑛 ∈ Fin)
18	16, 17	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → 𝒫 𝑛 ∈ Fin)
19		ficardom 9897	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑛 ∈ Fin → (card‘𝒫 𝑛) ∈ ω)
20		isinf 9204	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐴 ∈ Fin → ∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚))
21		breq2 5109	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (card‘𝒫 𝑛) → (𝑦 ≈ 𝑚 ↔ 𝑦 ≈ (card‘𝒫 𝑛)))
22	21	anbi2d 629	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (card‘𝒫 𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
23	22	exbidv 1924	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
24	23	rspcv 3577	. . . . . . . . . . . . . 14 ⊢ ((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
25	20, 24	syl5 34	. . . . . . . . . . . . 13 ⊢ ((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
26	18, 19, 25	3syl 18	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛))))
27		finnum 9884	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ Fin → 𝒫 𝑛 ∈ dom card)
28		cardid2 9889	. . . . . . . . . . . . . . 15 ⊢ (𝒫 𝑛 ∈ dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛)
29		entr 8946	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ≈ (card‘𝒫 𝑛) ∧ (card‘𝒫 𝑛) ≈ 𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)
30	29	expcom 414	. . . . . . . . . . . . . . 15 ⊢ ((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
31	18, 27, 28, 30	4syl 19	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛))
32	31	anim2d 612	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
33	32	eximdv 1920	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
34	26, 33	syld 47	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)))
35	1	neeq1i 3008	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅)
36		abn0 4340	. . . . . . . . . . . 12 ⊢ ({𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))
37	35, 36	bitri 274	. . . . . . . . . . 11 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))
38	34, 37	syl6ibr 251	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → 𝐵 ≠ ∅))
39	38	com12 32	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅))
40	39	adantr 481	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅))
41		rsp 3230	. . . . . . . . 9 ⊢ (∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
42	41	adantl 482	. . . . . . . 8 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)))
43	40, 42	mpdd 43	. . . . . . 7 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
44	15, 43	ralrimi 3240	. . . . . 6 ⊢ ((¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
45	44	3adant2 1131	. . . . 5 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
46	45	3expib 1122	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
47	46	eximdv 1920	. . 3 ⊢ (¬ 𝐴 ∈ Fin → (∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵))
48	12, 47	mpi 20	. 2 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)
49		axcc2 10373	. . . . 5 ⊢ ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
50		simp2 1137	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → 𝑐 Fn ω)
51		nfra1 3267	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵
52		nfra1 3267	. . . . . . . . . . 11 ⊢ Ⅎ𝑛∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))
53	51, 52	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
54		fvex 6855	. . . . . . . . . . . . . . . 16 ⊢ (𝑏‘𝑛) ∈ V
55		sseq1 3969	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ⊆ 𝐴 ↔ (𝑏‘𝑛) ⊆ 𝐴))
56		breq1 5108	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏‘𝑛) ≈ 𝒫 𝑛))
57	55, 56	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑏‘𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛)))
58	54, 57, 1	elab2 3634	. . . . . . . . . . . . . . 15 ⊢ ((𝑏‘𝑛) ∈ 𝐵 ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛))
59	58	simprbi 497	. . . . . . . . . . . . . 14 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ≈ 𝒫 𝑛)
60	59	ralimi 3086	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛)
61		fveq2 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (𝑏‘𝑛) = (𝑏‘𝑘))
62		pweq 4574	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘)
63	61, 62	breq12d 5118	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ (𝑏‘𝑘) ≈ 𝒫 𝑘))
64	63	cbvralvw 3225	. . . . . . . . . . . . . . 15 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘)
65		peano2 7827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
66		omelon 9582	. . . . . . . . . . . . . . . . . . 19 ⊢ ω ∈ On
67	66	onelssi 6432	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω)
68		ssralv 4010	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑛 ⊆ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
69	65, 67, 68	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘))
70		pwsdompw 10140	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))
71	70	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
72	69, 71	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)))
73		sdomdif 9069	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛) → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)
74	72, 73	syl6 35	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
75	64, 74	biimtrid 241	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
76	54	difexi 5285	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V
77		domtriomlem.3	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
78	77	fvmpt2 6959	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ω ∧ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V) → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
79	76, 78	mpan2 689	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
80	79	neeq1d 3003	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ ↔ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅))
81	75, 80	sylibrd 258	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛 → (𝐶‘𝑛) ≠ ∅))
82	60, 81	syl5com 31	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
83	82	adantr 481	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅))
84		rsp 3230	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
85	84	adantl 482	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
86	83, 85	mpdd 43	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
87	53, 86	ralrimi 3240	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
88	87	3adant2 1131	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
89	50, 88	jca 512	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
90	89	3expib 1122	. . . . . 6 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
91	90	eximdv 1920	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))))
92	49, 91	mpi 20	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
93		simp2 1137	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐 Fn ω)
94		nfra1 3267	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)
95	51, 94	nfan 1902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))
96		rsp 3230	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
97	96	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))
98		rsp 3230	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵))
99	98	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ∈ 𝐵))
100	79	eleq2d 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
101		eldifi 4086	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ (𝑏‘𝑛))
102	100, 101	syl6bi 252	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑛)))
103	58	simplbi 498	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ⊆ 𝐴)
104	103	sseld 3943	. . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴))
111	95, 110	ralrimi 3240	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
112	111	3adant2 1131	. . . . . . . . . 10 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)
113		ffnfv 7066	. . . . . . . . . 10 ⊢ (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴))
114	93, 112, 113	sylanbrc 583	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω⟶𝐴)
115		nfv 1917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑘 ∈ ω
116		nnord 7810	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ω → Ord 𝑘)
117		nnord 7810	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → Ord 𝑛)
118		ordtri3or 6349	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑘 ∧ Ord 𝑛) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
119	116, 117, 118	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘))
120		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → (𝑐‘𝑛) = (𝑐‘𝑘))
121		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗))
122	121	cbviunv 5000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗)
123		iuneq1 4970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 𝑘 → ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
124	122, 123	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
125	61, 124	difeq12d 4083	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) = ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
126	120, 125	eleq12d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) ↔ (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
127	126	rspccv 3578	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑘 ∈ ω → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
128	96, 100	mpbidi 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))))
129	94, 128	ralrimi 3240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
130	127, 129	syl11 33	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ω → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
131	130	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
132		eldifi 4086	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑘) ∈ (𝑏‘𝑘))
133		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ (𝑏‘𝑘) ↔ (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
134	132, 133	imbitrid 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
135	134	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
136	131, 135	syld 47	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)))
137	136	imp 407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))
138		ssiun2 5007	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑛 → (𝑏‘𝑘) ⊆ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
139	138	sseld 3943	. . . . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)))
145	144	eldifbd 3923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
146	145	3adant1 1130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))
147	141, 146	pm2.21dd 194	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
148	147	3exp 1119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
149		2a1 28	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
150		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 𝑛 → (𝑏‘𝑗) = (𝑏‘𝑛))
151	150	ssiun2s 5008	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝑘 → (𝑏‘𝑛) ⊆ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
152	151	sseld 3943	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
153	101, 152	syl5 34	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
154	144, 153	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
155	154	3impib 1116	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
156		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
157		eldifn 4087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
158	156, 157	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
159	158	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
160	131, 159	syld 47	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)))
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))))
162	161	3imp 1111	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗))
163	155, 162	pm2.21dd 194	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛)
164	163	3exp 1119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))
165	148, 149, 164	3jaoi 1427	. . . . . . . . . . . . . . . . 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 416	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))))
171	94, 115, 170	ralrimd 3247	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
172	171	ralrimiv 3142	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
173	172	3ad2ant3 1135	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))
174		dff13 7202	. . . . . . . . 9 ⊢ (𝑐:ω–1-1→𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))
175	114, 173, 174	sylanbrc 583	. . . . . . . 8 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω–1-1→𝐴)
176	175	19.8ad 2175	. . . . . . 7 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∃𝑐 𝑐:ω–1-1→𝐴)
177	2	brdom 8900	. . . . . . 7 ⊢ (ω ≼ 𝐴 ↔ ∃𝑐 𝑐:ω–1-1→𝐴)
178	176, 177	sylibr 233	. . . . . 6 ⊢ ((∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)
179	178	3expib 1122	. . . . 5 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
180	179	exlimdv 1936	. . . 4 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴))
181	92, 180	mpd 15	. . 3 ⊢ (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
182	181	exlimiv 1933	. 2 ⊢ (∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴)
183	48, 182	syl 17	1 ⊢ (¬ 𝐴 ∈ Fin → ω ≼ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713   ≠ wne 2943  ∀wral 3064  Vcvv 3445   ∖ cdif 3907   ⊆ wss 3910  ∅c0 4282  𝒫 cpw 4560  ∪ ciun 4954   class class class wbr 5105   ↦ cmpt 5188  dom cdm 5633  Ord word 6316  suc csuc 6319   Fn wfn 6491  ⟶wf 6492  –1-1→wf1 6493  ‘cfv 6496  ωcom 7802   ≈ cen 8880   ≼ cdom 8881   ≺ csdm 8882  Fincfn 8883  cardccrd 9871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cc 10371

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-dju 9837  df-card 9875

This theorem is referenced by:  domtriom  10379