Theorem comppfsc 22883

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 4567	. . . 4 ⊢ (𝑐 ∈ 𝒫 𝐽 → 𝑐 ⊆ 𝐽)
2		comppfsc.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
3	2	cmpcov 22740	. . . . . 6 ⊢ ((𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
4		elfpw 9298	. . . . . . . 8 ⊢ (𝑑 ∈ (𝒫 𝑐 ∩ Fin) ↔ (𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin))
5		finptfin 22869	. . . . . . . . . . 11 ⊢ (𝑑 ∈ Fin → 𝑑 ∈ PtFin)
6	5	anim1i 615	. . . . . . . . . 10 ⊢ ((𝑑 ∈ Fin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
7	6	anassrs 468	. . . . . . . . 9 ⊢ (((𝑑 ∈ Fin ∧ 𝑑 ⊆ 𝑐) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
8	7	ancom1s 651	. . . . . . . 8 ⊢ (((𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
9	4, 8	sylanb 581	. . . . . . 7 ⊢ ((𝑑 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
10	9	reximi2 3082	. . . . . 6 ⊢ (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))
11	3, 10	syl 17	. . . . 5 ⊢ ((𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))
12	11	3exp 1119	. . . 4 ⊢ (𝐽 ∈ Comp → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))
13	1, 12	syl5 34	. . 3 ⊢ (𝐽 ∈ Comp → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))
14	13	ralrimiv 3142	. 2 ⊢ (𝐽 ∈ Comp → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
15		elpwi 4567	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐽 → 𝑎 ⊆ 𝐽)
16		0elpw 5311	. . . . . . . . . . 11 ⊢ ∅ ∈ 𝒫 𝑎
17		0fin 9115	. . . . . . . . . . 11 ⊢ ∅ ∈ Fin
18	16, 17	elini 4153	. . . . . . . . . 10 ⊢ ∅ ∈ (𝒫 𝑎 ∩ Fin)
19		unieq 4876	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∪ ∅)
20		uni0 4896	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
21	19, 20	eqtrdi 2792	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∅)
22	21	rspceeqv 3595	. . . . . . . . . 10 ⊢ ((∅ ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
23	18, 22	mpan 688	. . . . . . . . 9 ⊢ (𝑋 = ∅ → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
24	23	a1i13 27	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
25		n0 4306	. . . . . . . . 9 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑋)
26		simp2 1137	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → 𝑋 = ∪ 𝑎)
27	26	eleq2d 2823	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑎))
28	27	biimpd 228	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → 𝑥 ∈ ∪ 𝑎))
29		eluni2 4869	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑎 ↔ ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠)
30	28, 29	syl6ib 250	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠))
31		simpl3 1193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑎 ⊆ 𝐽)
32		simprl 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝑎)
33	31, 32	sseldd 3945	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
34		elssuni 4898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ ∪ 𝐽)
35	34, 2	sseqtrrdi 3995	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ 𝑋)
36	33, 35	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ 𝑋)
37	36	ralrimivw 3147	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
38		iunss 5005	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
39	37, 38	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
40		ssequn1 4140	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
41	39, 40	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
42		simpl2 1192	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑎)
43		uniiun 5018	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑎 = ∪ 𝑝 ∈ 𝑎 𝑝
44	42, 43	eqtrdi 2792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑝 ∈ 𝑎 𝑝)
45	44	uneq2d 4123	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
46	41, 45	eqtr3d 2778	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
47		iunun 5053	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝)
48		vex 3449	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑠 ∈ V
49		vex 3449	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑝 ∈ V
50	48, 49	unex 7680	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∪ 𝑝) ∈ V
51	50	dfiun3 5921	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
52	47, 51	eqtr3i 2766	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
53	46, 52	eqtrdi 2792	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
54		simpll1 1212	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝐽 ∈ Top)
55	33	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑠 ∈ 𝐽)
56	31	sselda 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝐽)
57		unopn 22252	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ Top ∧ 𝑠 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽) → (𝑠 ∪ 𝑝) ∈ 𝐽)
58	54, 55, 56, 57	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → (𝑠 ∪ 𝑝) ∈ 𝐽)
59	58	fmpttd 7063	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)):𝑎⟶𝐽)
60	59	frnd 6676	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽)
61		elpw2g 5301	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
62	61	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
63	62	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
64	60, 63	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽)
65		unieq 4876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∪ 𝑐 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
66	65	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
67		sseq2 3970	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑑 ⊆ 𝑐 ↔ 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
68	67	anbi1d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
69	68	rexbidv 3175	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
70	66, 69	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) ↔ (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
71	70	rspcv 3577	. . . . . . . . . . . . . . 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 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑠)
75		ssel2 3939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
76	75	3ad2antl3 1187	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
77	76	adantrr 715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
78		elunii 4870	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 ∈ 𝐽) → 𝑥 ∈ ∪ 𝐽)
79	74, 77, 78	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ ∪ 𝐽)
80	79, 2	eleqtrrdi 2849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑋)
81	80	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ 𝑋)
82		simprr 771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑋 = ∪ 𝑑)
83	81, 82	eleqtrd 2840	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ ∪ 𝑑)
84		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑑 = ∪ 𝑑
85	84	ptfinfin 22870	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ∈ PtFin ∧ 𝑥 ∈ ∪ 𝑑) → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin)
86	85	expcom 414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ∪ 𝑑 → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
87	83, 86	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
88		simprl 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
89		elun1 4136	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝑠 → 𝑥 ∈ (𝑠 ∪ 𝑝))
90	89	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ (𝑠 ∪ 𝑝))
91	90	ralrimivw 3147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝))
92	50	rgenw 3068	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) ∈ V
93		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
94		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (𝑠 ∪ 𝑝) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑠 ∪ 𝑝)))
95	93, 94	ralrnmptw 7044	. . . . . . . . . . . . . . . . . . . . . . . 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 4010	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧))
100	88, 98, 99	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
101		rabid2 3436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ↔ ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
102	100, 101	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧})
103	102	eleq1d 2822	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin ↔ {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
104	103	biimprd 247	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ({𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin → 𝑑 ∈ Fin))
105	93	rnmpt 5910	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)}
106	88, 105	sseqtrdi 3994	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)})
107		ssabral 4019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)} ↔ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
108	106, 107	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
109		uneq2 4117	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑠 ∪ 𝑝) = (𝑠 ∪ (𝑓‘𝑞)))
110	109	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑞 = (𝑠 ∪ 𝑝) ↔ 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
111	110	ac6sfi 9231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Fin ∧ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)) → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
112	111	expcom 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
113	108, 112	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
114		frn 6675	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑑⟶𝑎 → ran 𝑓 ⊆ 𝑎)
115	114	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ran 𝑓 ⊆ 𝑎)
116	115	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝑎)
117	32	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝑎)
118	117	snssd 4769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝑎)
119	116, 118	unssd 4146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑎)
120		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑑 ∈ Fin)
121		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑⟶𝑎)
122	121	ffnd 6669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓 Fn 𝑑)
123		dffn4 6762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn 𝑑 ↔ 𝑓:𝑑–onto→ran 𝑓)
124	122, 123	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑–onto→ran 𝑓)
125		fofi 9282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑑 ∈ Fin ∧ 𝑓:𝑑–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
126	120, 124, 125	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ∈ Fin)
127		snfi 8988	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑠} ∈ Fin
128		unfi 9116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∈ Fin ∧ {𝑠} ∈ Fin) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
129	126, 127, 128	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
130		elfpw 9298	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ↔ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝑎 ∧ (ran 𝑓 ∪ {𝑠}) ∈ Fin))
131	119, 129, 130	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin))
132		simplrr 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ 𝑑)
133		uniiun 5018	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 𝑞
134		simprrr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))
135		iuneq2 4973	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 4133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ {𝑠} ⊆ (ran 𝑓 ∪ {𝑠})
140		vsnid 4623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑠 ∈ {𝑠}
141	139, 140	sselii 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑠 ∈ (ran 𝑓 ∪ {𝑠})
142		elssuni 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 ∈ (ran 𝑓 ∪ {𝑠}) → 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
143	141, 142	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
144		fvssunirn 6875	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑞) ⊆ ∪ ran 𝑓
145		ssun1 4132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑠})
146	145	unissi 4874	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∪ ran 𝑓 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
147	144, 146	sstri 3953	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘𝑞) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
148	143, 147	unssi 4145	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
149	148	rgenw 3068	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
150		iunss 5005	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}) ↔ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
151	149, 150	mpbir 230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
152	138, 151	eqsstrdi 3998	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
153	31	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑎 ⊆ 𝐽)
154	116, 153	sstrd 3954	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝐽)
155	33	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝐽)
156	155	snssd 4769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝐽)
157	154, 156	unssd 4146	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
158		uniss 4873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ ∪ 𝐽)
159	158, 2	sseqtrrdi 3995	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
160	157, 159	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
161	152, 160	eqssd 3961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ (ran 𝑓 ∪ {𝑠}))
162		unieq 4876	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (ran 𝑓 ∪ {𝑠}) → ∪ 𝑏 = ∪ (ran 𝑓 ∪ {𝑠}))
163	162	rspceeqv 3595	. . . . . . . . . . . . . . . . . . . . . 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 1936	. . . . . . . . . . . . . . . . . . 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 3150	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
173	73, 172	syld 47	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
174	173	rexlimdvaa 3153	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
175	30, 174	syld 47	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
176	175	exlimdv 1936	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑥 𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
177	25, 176	biimtrid 241	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 ≠ ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
178	24, 177	pm2.61dne 3031	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
179	15, 178	syl3an3 1165	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ∈ 𝒫 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
180	179	3exp 1119	. . . . 5 ⊢ (𝐽 ∈ Top → (𝑋 = ∪ 𝑎 → (𝑎 ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
181	180	com24 95	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑎 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))))
182	181	ralrimdv 3149	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
183	2	iscmp 22739	. . . 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 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  {crab 3407  Vcvv 3445   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  𝒫 cpw 4560  {csn 4586  ∪ cuni 4865  ∪ ciun 4954   ↦ cmpt 5188  ran crn 5634   Fn wfn 6491  ⟶wf 6492  –onto→wfo 6494  ‘cfv 6496  Fincfn 8883  Topctop 22242  Compccmp 22737  PtFincptfin 22854

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-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

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-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-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-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-om 7803  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-fin 8887  df-top 22243  df-cmp 22738  df-ptfin 22857

This theorem is referenced by: (None)