Theorem comppfsc 22789

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 4554	. . . 4 ⊢ (𝑐 ∈ 𝒫 𝐽 → 𝑐 ⊆ 𝐽)
2		comppfsc.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
3	2	cmpcov 22646	. . . . . 6 ⊢ ((𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
4		elfpw 9219	. . . . . . . 8 ⊢ (𝑑 ∈ (𝒫 𝑐 ∩ Fin) ↔ (𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin))
5		finptfin 22775	. . . . . . . . . . 11 ⊢ (𝑑 ∈ Fin → 𝑑 ∈ PtFin)
6	5	anim1i 615	. . . . . . . . . 10 ⊢ ((𝑑 ∈ Fin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
7	6	anassrs 468	. . . . . . . . 9 ⊢ (((𝑑 ∈ Fin ∧ 𝑑 ⊆ 𝑐) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
8	7	ancom1s 650	. . . . . . . 8 ⊢ (((𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
9	4, 8	sylanb 581	. . . . . . 7 ⊢ ((𝑑 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
10	9	reximi2 3078	. . . . . 6 ⊢ (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))
11	3, 10	syl 17	. . . . 5 ⊢ ((𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))
12	11	3exp 1118	. . . 4 ⊢ (𝐽 ∈ Comp → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))
13	1, 12	syl5 34	. . 3 ⊢ (𝐽 ∈ Comp → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))
14	13	ralrimiv 3138	. 2 ⊢ (𝐽 ∈ Comp → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
15		elpwi 4554	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐽 → 𝑎 ⊆ 𝐽)
16		0elpw 5298	. . . . . . . . . . 11 ⊢ ∅ ∈ 𝒫 𝑎
17		0fin 9036	. . . . . . . . . . 11 ⊢ ∅ ∈ Fin
18	16, 17	elini 4140	. . . . . . . . . 10 ⊢ ∅ ∈ (𝒫 𝑎 ∩ Fin)
19		unieq 4863	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∪ ∅)
20		uni0 4883	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
21	19, 20	eqtrdi 2792	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∅)
22	21	rspceeqv 3584	. . . . . . . . . 10 ⊢ ((∅ ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
23	18, 22	mpan 687	. . . . . . . . 9 ⊢ (𝑋 = ∅ → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
24	23	a1i13 27	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
25		n0 4293	. . . . . . . . 9 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑋)
26		simp2 1136	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → 𝑋 = ∪ 𝑎)
27	26	eleq2d 2822	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑎))
28	27	biimpd 228	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → 𝑥 ∈ ∪ 𝑎))
29		eluni2 4856	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑎 ↔ ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠)
30	28, 29	syl6ib 250	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠))
31		simpl3 1192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑎 ⊆ 𝐽)
32		simprl 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝑎)
33	31, 32	sseldd 3933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
34		elssuni 4885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ ∪ 𝐽)
35	34, 2	sseqtrrdi 3983	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ 𝑋)
36	33, 35	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ 𝑋)
37	36	ralrimivw 3143	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
38		iunss 4992	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
39	37, 38	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
40		ssequn1 4127	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
41	39, 40	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
42		simpl2 1191	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑎)
43		uniiun 5005	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑎 = ∪ 𝑝 ∈ 𝑎 𝑝
44	42, 43	eqtrdi 2792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑝 ∈ 𝑎 𝑝)
45	44	uneq2d 4110	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
46	41, 45	eqtr3d 2778	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
47		iunun 5040	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝)
48		vex 3445	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑠 ∈ V
49		vex 3445	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑝 ∈ V
50	48, 49	unex 7658	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∪ 𝑝) ∈ V
51	50	dfiun3 5907	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
52	47, 51	eqtr3i 2766	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
53	46, 52	eqtrdi 2792	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
54		simpll1 1211	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝐽 ∈ Top)
55	33	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑠 ∈ 𝐽)
56	31	sselda 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝐽)
57		unopn 22158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ Top ∧ 𝑠 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽) → (𝑠 ∪ 𝑝) ∈ 𝐽)
58	54, 55, 56, 57	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → (𝑠 ∪ 𝑝) ∈ 𝐽)
59	58	fmpttd 7045	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)):𝑎⟶𝐽)
60	59	frnd 6659	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽)
61		elpw2g 5288	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
62	61	3ad2ant1 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
63	62	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
64	60, 63	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽)
65		unieq 4863	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∪ 𝑐 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
66	65	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
67		sseq2 3958	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑑 ⊆ 𝑐 ↔ 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
68	67	anbi1d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
69	68	rexbidv 3171	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
70	66, 69	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) ↔ (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
71	70	rspcv 3566	. . . . . . . . . . . . . . 15 ⊢ (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
72	64, 71	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
73	53, 72	mpid 44	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
74		simprr 770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑠)
75		ssel2 3927	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
76	75	3ad2antl3 1186	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
77	76	adantrr 714	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
78		elunii 4857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 ∈ 𝐽) → 𝑥 ∈ ∪ 𝐽)
79	74, 77, 78	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ ∪ 𝐽)
80	79, 2	eleqtrrdi 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑋)
81	80	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ 𝑋)
82		simprr 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑋 = ∪ 𝑑)
83	81, 82	eleqtrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ ∪ 𝑑)
84		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑑 = ∪ 𝑑
85	84	ptfinfin 22776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ∈ PtFin ∧ 𝑥 ∈ ∪ 𝑑) → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin)
86	85	expcom 414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ∪ 𝑑 → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
87	83, 86	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
88		simprl 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
89		elun1 4123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝑠 → 𝑥 ∈ (𝑠 ∪ 𝑝))
90	89	ad2antll 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ (𝑠 ∪ 𝑝))
91	90	ralrimivw 3143	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝))
92	50	rgenw 3065	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) ∈ V
93		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
94		eleq2 2825	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (𝑠 ∪ 𝑝) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑠 ∪ 𝑝)))
95	93, 94	ralrnmptw 7026	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) ∈ V → (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 ↔ ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝)))
96	92, 95	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 ↔ ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝))
97	91, 96	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧)
98	97	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧)
99		ssralv 3998	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧))
100	88, 98, 99	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
101		rabid2 3432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ↔ ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
102	100, 101	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧})
103	102	eleq1d 2821	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin ↔ {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
104	103	biimprd 247	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ({𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin → 𝑑 ∈ Fin))
105	93	rnmpt 5896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)}
106	88, 105	sseqtrdi 3982	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)})
107		ssabral 4007	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)} ↔ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
108	106, 107	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
109		uneq2 4104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑠 ∪ 𝑝) = (𝑠 ∪ (𝑓‘𝑞)))
110	109	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑞 = (𝑠 ∪ 𝑝) ↔ 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
111	110	ac6sfi 9152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Fin ∧ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)) → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
112	111	expcom 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
113	108, 112	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
114		frn 6658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑑⟶𝑎 → ran 𝑓 ⊆ 𝑎)
115	114	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ran 𝑓 ⊆ 𝑎)
116	115	ad2antll 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝑎)
117	32	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝑎)
118	117	snssd 4756	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝑎)
119	116, 118	unssd 4133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑎)
120		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑑 ∈ Fin)
121		simprrl 778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑⟶𝑎)
122	121	ffnd 6652	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓 Fn 𝑑)
123		dffn4 6745	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn 𝑑 ↔ 𝑓:𝑑–onto→ran 𝑓)
124	122, 123	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑–onto→ran 𝑓)
125		fofi 9203	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑑 ∈ Fin ∧ 𝑓:𝑑–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
126	120, 124, 125	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ∈ Fin)
127		snfi 8909	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑠} ∈ Fin
128		unfi 9037	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∈ Fin ∧ {𝑠} ∈ Fin) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
129	126, 127, 128	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
130		elfpw 9219	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ↔ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝑎 ∧ (ran 𝑓 ∪ {𝑠}) ∈ Fin))
131	119, 129, 130	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin))
132		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ 𝑑)
133		uniiun 5005	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 𝑞
134		simprrr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))
135		iuneq2 4960	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
137	133, 136	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
138	132, 137	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
139		ssun2 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ {𝑠} ⊆ (ran 𝑓 ∪ {𝑠})
140		vsnid 4610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑠 ∈ {𝑠}
141	139, 140	sselii 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑠 ∈ (ran 𝑓 ∪ {𝑠})
142		elssuni 4885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 ∈ (ran 𝑓 ∪ {𝑠}) → 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
143	141, 142	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
144		fvssunirn 6858	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑞) ⊆ ∪ ran 𝑓
145		ssun1 4119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑠})
146	145	unissi 4861	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∪ ran 𝑓 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
147	144, 146	sstri 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘𝑞) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
148	143, 147	unssi 4132	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
149	148	rgenw 3065	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
150		iunss 4992	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}) ↔ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
151	149, 150	mpbir 230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
152	138, 151	eqsstrdi 3986	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
153	31	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑎 ⊆ 𝐽)
154	116, 153	sstrd 3942	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝐽)
155	33	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝐽)
156	155	snssd 4756	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝐽)
157	154, 156	unssd 4133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
158		uniss 4860	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ ∪ 𝐽)
159	158, 2	sseqtrrdi 3983	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
160	157, 159	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
161	152, 160	eqssd 3949	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ (ran 𝑓 ∪ {𝑠}))
162		unieq 4863	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (ran 𝑓 ∪ {𝑠}) → ∪ 𝑏 = ∪ (ran 𝑓 ∪ {𝑠}))
163	162	rspceeqv 3584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∪ (ran 𝑓 ∪ {𝑠})) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
164	131, 161, 163	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
165	164	expr 457	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ 𝑑 ∈ Fin) → ((𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
166	165	exlimdv 1935	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ 𝑑 ∈ Fin) → (∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
167	166	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → (∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
168	113, 167	mpdd 43	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
169	87, 104, 168	3syld 60	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
170	169	ex 413	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ((𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
171	170	com23 86	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (𝑑 ∈ PtFin → ((𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
172	171	rexlimdv 3146	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
173	73, 172	syld 47	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
174	173	rexlimdvaa 3149	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
175	30, 174	syld 47	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
176	175	exlimdv 1935	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑥 𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
177	25, 176	biimtrid 241	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 ≠ ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
178	24, 177	pm2.61dne 3028	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
179	15, 178	syl3an3 1164	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ∈ 𝒫 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
180	179	3exp 1118	. . . . 5 ⊢ (𝐽 ∈ Top → (𝑋 = ∪ 𝑎 → (𝑎 ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
181	180	com24 95	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑎 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
182	181	ralrimdv 3145	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
183	2	iscmp 22645	. . . 4 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
184	183	baibr 537	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) ↔ 𝐽 ∈ Comp))
185	182, 184	sylibd 238	. 2 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp))
186	14, 185	impbid2 225	1 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1540  ∃wex 1780   ∈ wcel 2105  {cab 2713   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3403  Vcvv 3441   ∪ cun 3896   ∩ cin 3897   ⊆ wss 3898  ∅c0 4269  𝒫 cpw 4547  {csn 4573  ∪ cuni 4852  ∪ ciun 4941   ↦ cmpt 5175  ran crn 5621   Fn wfn 6474  ⟶wf 6475  –onto→wfo 6477  ‘cfv 6479  Fincfn 8804  Topctop 22148  Compccmp 22643  PtFincptfin 22760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-om 7781  df-1o 8367  df-er 8569  df-en 8805  df-dom 8806  df-fin 8808  df-top 22149  df-cmp 22644  df-ptfin 22763

This theorem is referenced by: (None)