Theorem comppfsc 21549

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 4361	. . . 4 ⊢ (𝑐 ∈ 𝒫 𝐽 → 𝑐 ⊆ 𝐽)
2		comppfsc.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
3	2	cmpcov 21406	. . . . . 6 ⊢ ((𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
4		elfpw 8507	. . . . . . . 8 ⊢ (𝑑 ∈ (𝒫 𝑐 ∩ Fin) ↔ (𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin))
5		finptfin 21535	. . . . . . . . . . 11 ⊢ (𝑑 ∈ Fin → 𝑑 ∈ PtFin)
6	5	anim1i 604	. . . . . . . . . 10 ⊢ ((𝑑 ∈ Fin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
7	6	anassrs 455	. . . . . . . . 9 ⊢ (((𝑑 ∈ Fin ∧ 𝑑 ⊆ 𝑐) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
8	7	ancom1s 635	. . . . . . . 8 ⊢ (((𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
9	4, 8	sylanb 572	. . . . . . 7 ⊢ ((𝑑 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
10	9	reximi2 3197	. . . . . 6 ⊢ (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))
11	3, 10	syl 17	. . . . 5 ⊢ ((𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))
12	11	3exp 1141	. . . 4 ⊢ (𝐽 ∈ Comp → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))
13	1, 12	syl5 34	. . 3 ⊢ (𝐽 ∈ Comp → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))
14	13	ralrimiv 3153	. 2 ⊢ (𝐽 ∈ Comp → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
15		elpwi 4361	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐽 → 𝑎 ⊆ 𝐽)
16		0elpw 5026	. . . . . . . . . . . 12 ⊢ ∅ ∈ 𝒫 𝑎
17		0fin 8427	. . . . . . . . . . . 12 ⊢ ∅ ∈ Fin
18		elin 3995	. . . . . . . . . . . 12 ⊢ (∅ ∈ (𝒫 𝑎 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑎 ∧ ∅ ∈ Fin))
19	16, 17, 18	mpbir2an 693	. . . . . . . . . . 11 ⊢ ∅ ∈ (𝒫 𝑎 ∩ Fin)
20		unieq 4638	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∪ ∅)
21		uni0 4659	. . . . . . . . . . . . 13 ⊢ ∪ ∅ = ∅
22	20, 21	syl6eq 2856	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∅)
23	22	rspceeqv 3520	. . . . . . . . . . 11 ⊢ ((∅ ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
24	19, 23	mpan 673	. . . . . . . . . 10 ⊢ (𝑋 = ∅ → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
25	24	a1d 25	. . . . . . . . 9 ⊢ (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
26	25	a1i 11	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
27		n0 4132	. . . . . . . . 9 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑋)
28		simp2 1160	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → 𝑋 = ∪ 𝑎)
29	28	eleq2d 2871	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑎))
30	29	biimpd 220	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → 𝑥 ∈ ∪ 𝑎))
31		eluni2 4634	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑎 ↔ ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠)
32	30, 31	syl6ib 242	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠))
33		simpl3 1239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑎 ⊆ 𝐽)
34		simprl 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝑎)
35	33, 34	sseldd 3799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
36		elssuni 4661	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ ∪ 𝐽)
37	36, 2	syl6sseqr 3849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ 𝑋)
38	35, 37	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ 𝑋)
39	38	ralrimivw 3155	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
40		iunss 4753	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
41	39, 40	sylibr 225	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
42		ssequn1 3982	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
43	41, 42	sylib 209	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
44		simpl2 1237	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑎)
45		uniiun 4765	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑎 = ∪ 𝑝 ∈ 𝑎 𝑝
46	44, 45	syl6eq 2856	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑝 ∈ 𝑎 𝑝)
47	46	uneq2d 3966	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
48	43, 47	eqtr3d 2842	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
49		iunun 4796	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝)
50		vex 3394	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑠 ∈ V
51		vex 3394	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑝 ∈ V
52	50, 51	unex 7186	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∪ 𝑝) ∈ V
53	52	dfiun3 5581	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
54	49, 53	eqtr3i 2830	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
55	48, 54	syl6eq 2856	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
56		simpll1 1262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝐽 ∈ Top)
57	35	adantr 468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑠 ∈ 𝐽)
58	33	sselda 3798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝐽)
59		unopn 20921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ Top ∧ 𝑠 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽) → (𝑠 ∪ 𝑝) ∈ 𝐽)
60	56, 57, 58, 59	syl3anc 1483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → (𝑠 ∪ 𝑝) ∈ 𝐽)
61	60	fmpttd 6607	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)):𝑎⟶𝐽)
62	61	frnd 6263	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽)
63		elpw2g 5019	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
64	63	3ad2ant1 1156	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
65	64	adantr 468	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
66	62, 65	mpbird 248	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽)
67		unieq 4638	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∪ 𝑐 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
68	67	eqeq2d 2816	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
69		sseq2 3824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑑 ⊆ 𝑐 ↔ 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
70	69	anbi1d 617	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
71	70	rexbidv 3240	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
72	68, 71	imbi12d 335	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) ↔ (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
73	72	rspcv 3498	. . . . . . . . . . . . . . 15 ⊢ (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
74	66, 73	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
75	55, 74	mpid 44	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
76		simprr 780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑠)
77		ssel2 3793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
78	77	3ad2antl3 1231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
79	78	adantrr 699	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
80		elunii 4635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 ∈ 𝐽) → 𝑥 ∈ ∪ 𝐽)
81	76, 79, 80	syl2anc 575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ ∪ 𝐽)
82	81, 2	syl6eleqr 2896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑋)
83	82	adantr 468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ 𝑋)
84		simprr 780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑋 = ∪ 𝑑)
85	83, 84	eleqtrd 2887	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ ∪ 𝑑)
86		eqid 2806	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑑 = ∪ 𝑑
87	86	ptfinfin 21536	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ∈ PtFin ∧ 𝑥 ∈ ∪ 𝑑) → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin)
88	87	expcom 400	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ∪ 𝑑 → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
89	85, 88	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
90		simprl 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
91		elun1 3979	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝑠 → 𝑥 ∈ (𝑠 ∪ 𝑝))
92	91	ad2antll 711	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ (𝑠 ∪ 𝑝))
93	92	ralrimivw 3155	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝))
94	52	rgenw 3112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) ∈ V
95		eqid 2806	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
96		eleq2 2874	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (𝑠 ∪ 𝑝) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑠 ∪ 𝑝)))
97	95, 96	ralrnmpt 6590	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) ∈ V → (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 ↔ ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝)))
98	94, 97	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 ↔ ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝))
99	93, 98	sylibr 225	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧)
100	99	adantr 468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧)
101		ssralv 3863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧))
102	90, 100, 101	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
103		rabid2 3307	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ↔ ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
104	102, 103	sylibr 225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧})
105	104	eleq1d 2870	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin ↔ {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
106	105	biimprd 239	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ({𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin → 𝑑 ∈ Fin))
107	95	rnmpt 5572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)}
108	90, 107	syl6sseq 3848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)})
109		ssabral 3870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)} ↔ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
110	108, 109	sylib 209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
111		uneq2 3960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑠 ∪ 𝑝) = (𝑠 ∪ (𝑓‘𝑞)))
112	111	eqeq2d 2816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑞 = (𝑠 ∪ 𝑝) ↔ 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
113	112	ac6sfi 8443	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Fin ∧ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)) → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
114	113	expcom 400	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
115	110, 114	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
116		frn 6262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑑⟶𝑎 → ran 𝑓 ⊆ 𝑎)
117	116	adantr 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ran 𝑓 ⊆ 𝑎)
118	117	ad2antll 711	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝑎)
119	34	ad2antrr 708	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝑎)
120	119	snssd 4530	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝑎)
121	118, 120	unssd 3988	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑎)
122		simprl 778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑑 ∈ Fin)
123		simprrl 790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑⟶𝑎)
124	123	ffnd 6257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓 Fn 𝑑)
125		dffn4 6337	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn 𝑑 ↔ 𝑓:𝑑–onto→ran 𝑓)
126	124, 125	sylib 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑–onto→ran 𝑓)
127		fofi 8491	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑑 ∈ Fin ∧ 𝑓:𝑑–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
128	122, 126, 127	syl2anc 575	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ∈ Fin)
129		snfi 8277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑠} ∈ Fin
130		unfi 8466	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∈ Fin ∧ {𝑠} ∈ Fin) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
131	128, 129, 130	sylancl 576	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
132		elfpw 8507	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ↔ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝑎 ∧ (ran 𝑓 ∪ {𝑠}) ∈ Fin))
133	121, 131, 132	sylanbrc 574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin))
134		simplrr 787	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ 𝑑)
135		uniiun 4765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 𝑞
136		simprrr 791	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))
137		iuneq2 4729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
138	136, 137	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
139	135, 138	syl5eq 2852	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
140	134, 139	eqtrd 2840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
141		ssun2 3976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ {𝑠} ⊆ (ran 𝑓 ∪ {𝑠})
142		vsnid 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑠 ∈ {𝑠}
143	141, 142	sselii 3795	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑠 ∈ (ran 𝑓 ∪ {𝑠})
144		elssuni 4661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 ∈ (ran 𝑓 ∪ {𝑠}) → 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
145	143, 144	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
146		fvssunirn 6437	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑞) ⊆ ∪ ran 𝑓
147		ssun1 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑠})
148	147	unissi 4655	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∪ ran 𝑓 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
149	146, 148	sstri 3807	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘𝑞) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
150	145, 149	unssi 3987	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
151	150	rgenw 3112	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
152		iunss 4753	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}) ↔ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
153	151, 152	mpbir 222	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
154	140, 153	syl6eqss 3852	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
155	33	ad2antrr 708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑎 ⊆ 𝐽)
156	118, 155	sstrd 3808	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝐽)
157	35	ad2antrr 708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝐽)
158	157	snssd 4530	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝐽)
159	156, 158	unssd 3988	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
160		uniss 4653	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ ∪ 𝐽)
161	160, 2	syl6sseqr 3849	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
162	159, 161	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
163	154, 162	eqssd 3815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ (ran 𝑓 ∪ {𝑠}))
164		unieq 4638	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (ran 𝑓 ∪ {𝑠}) → ∪ 𝑏 = ∪ (ran 𝑓 ∪ {𝑠}))
165	164	rspceeqv 3520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∪ (ran 𝑓 ∪ {𝑠})) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
166	133, 163, 165	syl2anc 575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
167	166	expr 446	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ 𝑑 ∈ Fin) → ((𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
168	167	exlimdv 2024	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ 𝑑 ∈ Fin) → (∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
169	168	ex 399	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → (∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
170	115, 169	mpdd 43	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
171	89, 106, 170	3syld 60	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
172	171	ex 399	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ((𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
173	172	com23 86	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (𝑑 ∈ PtFin → ((𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
174	173	rexlimdv 3218	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
175	75, 174	syld 47	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
176	175	rexlimdvaa 3220	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
177	32, 176	syld 47	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
178	177	exlimdv 2024	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑥 𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
179	27, 178	syl5bi 233	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 ≠ ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
180	26, 179	pm2.61dne 3064	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
181	15, 180	syl3an3 1198	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ∈ 𝒫 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
182	181	3exp 1141	. . . . 5 ⊢ (𝐽 ∈ Top → (𝑋 = ∪ 𝑎 → (𝑎 ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
183	182	com24 95	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑎 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
184	183	ralrimdv 3156	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
185	2	iscmp 21405	. . . 4 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
186	185	baibr 528	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) ↔ 𝐽 ∈ Comp))
187	184, 186	sylibd 230	. 2 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp))
188	14, 187	impbid2 217	1 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∧ w3a 1100   = wceq 1637  ∃wex 1859   ∈ wcel 2156  {cab 2792   ≠ wne 2978  ∀wral 3096  ∃wrex 3097  {crab 3100  Vcvv 3391   ∪ cun 3767   ∩ cin 3768   ⊆ wss 3769  ∅c0 4116  𝒫 cpw 4351  {csn 4370  ∪ cuni 4630  ∪ ciun 4712   ↦ cmpt 4923  ran crn 5312   Fn wfn 6096  ⟶wf 6097  –onto→wfo 6099  ‘cfv 6101  Fincfn 8192  Topctop 20911  Compccmp 21403  PtFincptfin 21520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-oadd 7800  df-er 7979  df-en 8193  df-dom 8194  df-fin 8196  df-top 20912  df-cmp 21404  df-ptfin 21523

This theorem is referenced by: (None)