Theorem comppfsc 21145

Description: A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)

Hypothesis

Ref	Expression
comppfsc.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
comppfsc	⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))

Distinct variable groups:   𝑐,𝑑,𝐽   𝑋,𝑐,𝑑

Proof of Theorem comppfsc

Dummy variables 𝑎 𝑏 𝑓 𝑝 𝑞 𝑠 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpwi 4117	. . . 4 ⊢ (𝑐 ∈ 𝒫 𝐽 → 𝑐 ⊆ 𝐽)
2		comppfsc.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
3	2	cmpcov 21002	. . . . . 6 ⊢ ((𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
4		elfpw 8151	. . . . . . . 8 ⊢ (𝑑 ∈ (𝒫 𝑐 ∩ Fin) ↔ (𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin))
5		finptfin 21131	. . . . . . . . . . 11 ⊢ (𝑑 ∈ Fin → 𝑑 ∈ PtFin)
6	5	anim1i 590	. . . . . . . . . 10 ⊢ ((𝑑 ∈ Fin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
7	6	anassrs 678	. . . . . . . . 9 ⊢ (((𝑑 ∈ Fin ∧ 𝑑 ⊆ 𝑐) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
8	7	ancom1s 843	. . . . . . . 8 ⊢ (((𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
9	4, 8	sylanb 488	. . . . . . 7 ⊢ ((𝑑 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
10	9	reximi2 2993	. . . . . 6 ⊢ (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))
11	3, 10	syl 17	. . . . 5 ⊢ ((𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))
12	11	3exp 1256	. . . 4 ⊢ (𝐽 ∈ Comp → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))
13	1, 12	syl5 33	. . 3 ⊢ (𝐽 ∈ Comp → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))
14	13	ralrimiv 2948	. 2 ⊢ (𝐽 ∈ Comp → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
15		elpwi 4117	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐽 → 𝑎 ⊆ 𝐽)
16		0elpw 4760	. . . . . . . . . . . 12 ⊢ ∅ ∈ 𝒫 𝑎
17		0fin 8073	. . . . . . . . . . . 12 ⊢ ∅ ∈ Fin
18		elin 3758	. . . . . . . . . . . 12 ⊢ (∅ ∈ (𝒫 𝑎 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑎 ∧ ∅ ∈ Fin))
19	16, 17, 18	mpbir2an 957	. . . . . . . . . . 11 ⊢ ∅ ∈ (𝒫 𝑎 ∩ Fin)
20		unieq 4380	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∪ ∅)
21		uni0 4401	. . . . . . . . . . . . . 14 ⊢ ∪ ∅ = ∅
22	20, 21	syl6eq 2660	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∅)
23	22	eqeq2d 2620	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → (𝑋 = ∪ 𝑏 ↔ 𝑋 = ∅))
24	23	rspcev 3282	. . . . . . . . . . 11 ⊢ ((∅ ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
25	19, 24	mpan 702	. . . . . . . . . 10 ⊢ (𝑋 = ∅ → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
26	25	a1d 25	. . . . . . . . 9 ⊢ (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
27	26	a1i 11	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
28		n0 3890	. . . . . . . . 9 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑋)
29		simp2 1055	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → 𝑋 = ∪ 𝑎)
30	29	eleq2d 2673	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑎))
31	30	biimpd 218	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → 𝑥 ∈ ∪ 𝑎))
32		eluni2 4376	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑎 ↔ ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠)
33	31, 32	syl6ib 240	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠))
34		simpl3 1059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑎 ⊆ 𝐽)
35		simprl 790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝑎)
36	34, 35	sseldd 3569	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
37		elssuni 4403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ ∪ 𝐽)
38	37, 2	syl6sseqr 3615	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ 𝑋)
39	36, 38	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ 𝑋)
40	39	ralrimivw 2950	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
41		iunss 4497	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
42	40, 41	sylibr 223	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
43		ssequn1 3745	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
44	42, 43	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
45		simpl2 1058	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑎)
46		uniiun 4509	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑎 = ∪ 𝑝 ∈ 𝑎 𝑝
47	45, 46	syl6eq 2660	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑝 ∈ 𝑎 𝑝)
48	47	uneq2d 3729	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
49	44, 48	eqtr3d 2646	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
50		iunun 4540	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝)
51		vex 3176	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑠 ∈ V
52		vex 3176	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑝 ∈ V
53	51, 52	unex 6854	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∪ 𝑝) ∈ V
54	53	dfiun3 5301	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
55	50, 54	eqtr3i 2634	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
56	49, 55	syl6eq 2660	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
57		simpll1 1093	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝐽 ∈ Top)
58	36	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑠 ∈ 𝐽)
59	34	sselda 3568	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝐽)
60		unopn 20533	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ Top ∧ 𝑠 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽) → (𝑠 ∪ 𝑝) ∈ 𝐽)
61	57, 58, 59, 60	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → (𝑠 ∪ 𝑝) ∈ 𝐽)
62		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
63	61, 62	fmptd 6292	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)):𝑎⟶𝐽)
64		frn 5966	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)):𝑎⟶𝐽 → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽)
65	63, 64	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽)
66		elpw2g 4754	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
67	66	3ad2ant1 1075	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
68	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
69	65, 68	mpbird 246	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽)
70		unieq 4380	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∪ 𝑐 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
71	70	eqeq2d 2620	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
72		sseq2 3590	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑑 ⊆ 𝑐 ↔ 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
73	72	anbi1d 737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
74	73	rexbidv 3034	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
75	71, 74	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) ↔ (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
76	75	rspcv 3278	. . . . . . . . . . . . . . 15 ⊢ (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
77	69, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
78	56, 77	mpid 43	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
79		simprr 792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑠)
80		ssel2 3563	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
81	80	3ad2antl3 1218	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
82	81	adantrr 749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
83		elunii 4377	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 ∈ 𝐽) → 𝑥 ∈ ∪ 𝐽)
84	79, 82, 83	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ ∪ 𝐽)
85	84, 2	syl6eleqr 2699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑋)
86	85	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ 𝑋)
87		simprr 792	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑋 = ∪ 𝑑)
88	86, 87	eleqtrd 2690	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ ∪ 𝑑)
89		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑑 = ∪ 𝑑
90	89	ptfinfin 21132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ∈ PtFin ∧ 𝑥 ∈ ∪ 𝑑) → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin)
91	90	expcom 450	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ∪ 𝑑 → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
92	88, 91	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
93		simprl 790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
94		elun1 3742	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝑠 → 𝑥 ∈ (𝑠 ∪ 𝑝))
95	94	ad2antll 761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ (𝑠 ∪ 𝑝))
96	95	ralrimivw 2950	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝))
97	53	rgenw 2908	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) ∈ V
98		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (𝑠 ∪ 𝑝) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑠 ∪ 𝑝)))
99	62, 98	ralrnmpt 6276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) ∈ V → (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 ↔ ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝)))
100	97, 99	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 ↔ ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝))
101	96, 100	sylibr 223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧)
102	101	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧)
103		ssralv 3629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧))
104	93, 102, 103	sylc 63	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
105		rabid2 3096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ↔ ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
106	104, 105	sylibr 223	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧})
107	106	eleq1d 2672	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin ↔ {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
108	107	biimprd 237	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ({𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin → 𝑑 ∈ Fin))
109	62	rnmpt 5292	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)}
110	93, 109	syl6sseq 3614	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)})
111		ssabral 3636	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)} ↔ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
112	110, 111	sylib 207	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
113		uneq2 3723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑠 ∪ 𝑝) = (𝑠 ∪ (𝑓‘𝑞)))
114	113	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑞 = (𝑠 ∪ 𝑝) ↔ 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
115	114	ac6sfi 8089	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Fin ∧ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)) → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
116	115	expcom 450	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
117	112, 116	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
118		frn 5966	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑑⟶𝑎 → ran 𝑓 ⊆ 𝑎)
119	118	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ran 𝑓 ⊆ 𝑎)
120	119	ad2antll 761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝑎)
121	35	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝑎)
122	121	snssd 4281	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝑎)
123	120, 122	unssd 3751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑎)
124		simprl 790	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑑 ∈ Fin)
125		simprrl 800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑⟶𝑎)
126		ffn 5958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓:𝑑⟶𝑎 → 𝑓 Fn 𝑑)
127	125, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓 Fn 𝑑)
128		dffn4 6034	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn 𝑑 ↔ 𝑓:𝑑–onto→ran 𝑓)
129	127, 128	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑–onto→ran 𝑓)
130		fofi 8135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑑 ∈ Fin ∧ 𝑓:𝑑–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
131	124, 129, 130	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ∈ Fin)
132		snfi 7923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑠} ∈ Fin
133		unfi 8112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∈ Fin ∧ {𝑠} ∈ Fin) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
134	131, 132, 133	sylancl 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
135		elfpw 8151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ↔ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝑎 ∧ (ran 𝑓 ∪ {𝑠}) ∈ Fin))
136	123, 134, 135	sylanbrc 695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin))
137		simplrr 797	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ 𝑑)
138		uniiun 4509	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 𝑞
139		simprrr 801	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))
140		iuneq2 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
141	139, 140	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
142	138, 141	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
143	137, 142	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
144		ssun2 3739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ {𝑠} ⊆ (ran 𝑓 ∪ {𝑠})
145		vsnid 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑠 ∈ {𝑠}
146	144, 145	sselii 3565	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑠 ∈ (ran 𝑓 ∪ {𝑠})
147		elssuni 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 ∈ (ran 𝑓 ∪ {𝑠}) → 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
148	146, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
149		fvssunirn 6127	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑞) ⊆ ∪ ran 𝑓
150		ssun1 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑠})
151	150	unissi 4397	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∪ ran 𝑓 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
152	149, 151	sstri 3577	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘𝑞) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
153	148, 152	unssi 3750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
154	153	rgenw 2908	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
155		iunss 4497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}) ↔ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
156	154, 155	mpbir 220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
157	143, 156	syl6eqss 3618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
158	34	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑎 ⊆ 𝐽)
159	120, 158	sstrd 3578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝐽)
160	36	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝐽)
161	160	snssd 4281	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝐽)
162	159, 161	unssd 3751	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
163		uniss 4394	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ ∪ 𝐽)
164	163, 2	syl6sseqr 3615	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
165	162, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
166	157, 165	eqssd 3585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ (ran 𝑓 ∪ {𝑠}))
167		unieq 4380	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = (ran 𝑓 ∪ {𝑠}) → ∪ 𝑏 = ∪ (ran 𝑓 ∪ {𝑠}))
168	167	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (ran 𝑓 ∪ {𝑠}) → (𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ (ran 𝑓 ∪ {𝑠})))
169	168	rspcev 3282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∪ (ran 𝑓 ∪ {𝑠})) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
170	136, 166, 169	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
171	170	expr 641	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ 𝑑 ∈ Fin) → ((𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
172	171	exlimdv 1848	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ 𝑑 ∈ Fin) → (∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
173	172	ex 449	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → (∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
174	117, 173	mpdd 42	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
175	92, 108, 174	3syld 58	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
176	175	ex 449	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ((𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
177	176	com23 84	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (𝑑 ∈ PtFin → ((𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
178	177	rexlimdv 3012	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
179	78, 178	syld 46	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
180	179	rexlimdvaa 3014	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
181	33, 180	syld 46	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
182	181	exlimdv 1848	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑥 𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
183	28, 182	syl5bi 231	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 ≠ ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
184	27, 183	pm2.61dne 2868	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
185	15, 184	syl3an3 1353	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ∈ 𝒫 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
186	185	3exp 1256	. . . . 5 ⊢ (𝐽 ∈ Top → (𝑋 = ∪ 𝑎 → (𝑎 ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
187	186	com24 93	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑎 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
188	187	ralrimdv 2951	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
189	2	iscmp 21001	. . . 4 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
190	189	baibr 943	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) ↔ 𝐽 ∈ Comp))
191	188, 190	sylibd 228	. 2 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp))
192	14, 191	impbid2 215	1 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372  ∪ ciun 4455   ↦ cmpt 4643  ran crn 5039   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  Fincfn 7841  Topctop 20517  Compccmp 20999  PtFincptfin 21116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-fin 7845  df-top 20521  df-cmp 21000  df-ptfin 21119

This theorem is referenced by: (None)