Theorem comppfsc 23419

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 4570	. . . 4 ⊢ (𝑐 ∈ 𝒫 𝐽 → 𝑐 ⊆ 𝐽)
2		comppfsc.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
3	2	cmpcov 23276	. . . . . 6 ⊢ ((𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)
4		elfpw 9305	. . . . . . . 8 ⊢ (𝑑 ∈ (𝒫 𝑐 ∩ Fin) ↔ (𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin))
5		finptfin 23405	. . . . . . . . . . 11 ⊢ (𝑑 ∈ Fin → 𝑑 ∈ PtFin)
6	5	anim1i 615	. . . . . . . . . 10 ⊢ ((𝑑 ∈ Fin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
7	6	anassrs 467	. . . . . . . . 9 ⊢ (((𝑑 ∈ Fin ∧ 𝑑 ⊆ 𝑐) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
8	7	ancom1s 653	. . . . . . . 8 ⊢ (((𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
9	4, 8	sylanb 581	. . . . . . 7 ⊢ ((𝑑 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
10	9	reximi2 3062	. . . . . 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 3124	. 2 ⊢ (𝐽 ∈ Comp → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))
15		elpwi 4570	. . . . . . 7 ⊢ (𝑎 ∈ 𝒫 𝐽 → 𝑎 ⊆ 𝐽)
16		0elpw 5311	. . . . . . . . . . 11 ⊢ ∅ ∈ 𝒫 𝑎
17		0fi 9013	. . . . . . . . . . 11 ⊢ ∅ ∈ Fin
18	16, 17	elini 4162	. . . . . . . . . 10 ⊢ ∅ ∈ (𝒫 𝑎 ∩ Fin)
19		unieq 4882	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∪ ∅)
20		uni0 4899	. . . . . . . . . . . 12 ⊢ ∪ ∅ = ∅
21	19, 20	eqtrdi 2780	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → ∪ 𝑏 = ∅)
22	21	rspceeqv 3611	. . . . . . . . . 10 ⊢ ((∅ ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
23	18, 22	mpan 690	. . . . . . . . 9 ⊢ (𝑋 = ∅ → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
24	23	a1i13 27	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
25		n0 4316	. . . . . . . . 9 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑋)
26		simp2 1137	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → 𝑋 = ∪ 𝑎)
27	26	eleq2d 2814	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑎))
28	27	biimpd 229	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → 𝑥 ∈ ∪ 𝑎))
29		eluni2 4875	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑎 ↔ ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠)
30	28, 29	imbitrdi 251	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → ∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠))
31		simpl3 1194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑎 ⊆ 𝐽)
32		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝑎)
33	31, 32	sseldd 3947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
34		elssuni 4901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ ∪ 𝐽)
35	34, 2	sseqtrrdi 3988	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝐽 → 𝑠 ⊆ 𝑋)
36	33, 35	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ⊆ 𝑋)
37	36	ralrimivw 3129	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
38		iunss 5009	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ ∀𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
39	37, 38	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋)
40		ssequn1 4149	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
41	39, 40	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = 𝑋)
42		simpl2 1193	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑎)
43		uniiun 5022	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑎 = ∪ 𝑝 ∈ 𝑎 𝑝
44	42, 43	eqtrdi 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ 𝑝 ∈ 𝑎 𝑝)
45	44	uneq2d 4131	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
46	41, 45	eqtr3d 2766	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝))
47		iunun 5057	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝)
48		vex 3451	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑠 ∈ V
49		vex 3451	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑝 ∈ V
50	48, 49	unex 7720	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∪ 𝑝) ∈ V
51	50	dfiun3 5933	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
52	47, 51	eqtr3i 2754	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝) = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
53	46, 52	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
54		simpll1 1213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝐽 ∈ Top)
55	33	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑠 ∈ 𝐽)
56	31	sselda 3946	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝐽)
57		unopn 22790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ Top ∧ 𝑠 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽) → (𝑠 ∪ 𝑝) ∈ 𝐽)
58	54, 55, 56, 57	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ 𝑝 ∈ 𝑎) → (𝑠 ∪ 𝑝) ∈ 𝐽)
59	58	fmpttd 7087	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)):𝑎⟶𝐽)
60	59	frnd 6696	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽)
61		elpw2g 5288	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
62	61	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
63	62	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ⊆ 𝐽))
64	60, 63	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∈ 𝒫 𝐽)
65		unieq 4882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∪ 𝑐 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
66	65	eqeq2d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
67		sseq2 3973	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (𝑑 ⊆ 𝑐 ↔ 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))))
68	67	anbi1d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
69	68	rexbidv 3157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑) ↔ ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)))
70	66, 69	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ((𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) ↔ (𝑋 = ∪ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑))))
71	70	rspcv 3584	. . . . . . . . . . . . . . 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 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑠)
75		ssel2 3941	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ⊆ 𝐽 ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
76	75	3ad2antl3 1188	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ 𝑠 ∈ 𝑎) → 𝑠 ∈ 𝐽)
77	76	adantrr 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑠 ∈ 𝐽)
78		elunii 4876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 ∈ 𝐽) → 𝑥 ∈ ∪ 𝐽)
79	74, 77, 78	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ ∪ 𝐽)
80	79, 2	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ 𝑋)
81	80	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ 𝑋)
82		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑋 = ∪ 𝑑)
83	81, 82	eleqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑥 ∈ ∪ 𝑑)
84		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑑 = ∪ 𝑑
85	84	ptfinfin 23406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ∈ PtFin ∧ 𝑥 ∈ ∪ 𝑑) → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin)
86	85	expcom 413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ∪ 𝑑 → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
87	83, 86	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ PtFin → {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
88		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)))
89		elun1 4145	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝑠 → 𝑥 ∈ (𝑠 ∪ 𝑝))
90	89	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → 𝑥 ∈ (𝑠 ∪ 𝑝))
91	90	ralrimivw 3129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝))
92	50	rgenw 3048	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) ∈ V
93		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))
94		eleq2 2817	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = (𝑠 ∪ 𝑝) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝑠 ∪ 𝑝)))
95	93, 94	ralrnmptw 7066	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑝 ∈ 𝑎 (𝑠 ∪ 𝑝) ∈ V → (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 ↔ ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝)))
96	92, 95	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 ↔ ∀𝑝 ∈ 𝑎 𝑥 ∈ (𝑠 ∪ 𝑝))
97	91, 96	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧)
98	97	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧)
99		ssralv 4015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) → (∀𝑧 ∈ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝))𝑥 ∈ 𝑧 → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧))
100	88, 98, 99	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
101		rabid2 3439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ↔ ∀𝑧 ∈ 𝑑 𝑥 ∈ 𝑧)
102	100, 101	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 = {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧})
103	102	eleq1d 2813	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin ↔ {𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin))
104	103	biimprd 248	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ({𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧} ∈ Fin → 𝑑 ∈ Fin))
105	93	rnmpt 5921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) = {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)}
106	88, 105	sseqtrdi 3987	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → 𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)})
107		ssabral 4028	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ⊆ {𝑞 ∣ ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)} ↔ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
108	106, 107	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝))
109		uneq2 4125	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑠 ∪ 𝑝) = (𝑠 ∪ (𝑓‘𝑞)))
110	109	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = (𝑓‘𝑞) → (𝑞 = (𝑠 ∪ 𝑝) ↔ 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
111	110	ac6sfi 9231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ Fin ∧ ∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝)) → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))
112	111	expcom 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑞 ∈ 𝑑 ∃𝑝 ∈ 𝑎 𝑞 = (𝑠 ∪ 𝑝) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
113	108, 112	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))))
114		frn 6695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑑⟶𝑎 → ran 𝑓 ⊆ 𝑎)
115	114	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ran 𝑓 ⊆ 𝑎)
116	115	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝑎)
117	32	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝑎)
118	117	snssd 4773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝑎)
119	116, 118	unssd 4155	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑎)
120		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑑 ∈ Fin)
121		simprrl 780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑⟶𝑎)
122	121	ffnd 6689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓 Fn 𝑑)
123		dffn4 6778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 Fn 𝑑 ↔ 𝑓:𝑑–onto→ran 𝑓)
124	122, 123	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑓:𝑑–onto→ran 𝑓)
125		fofi 9262	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑑 ∈ Fin ∧ 𝑓:𝑑–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
126	120, 124, 125	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ∈ Fin)
127		snfi 9014	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑠} ∈ Fin
128		unfi 9135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∈ Fin ∧ {𝑠} ∈ Fin) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
129	126, 127, 128	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
130		elfpw 9305	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ↔ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝑎 ∧ (ran 𝑓 ∪ {𝑠}) ∈ Fin))
131	119, 129, 130	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin))
132		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ 𝑑)
133		uniiun 5022	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 𝑞
134		simprrr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)))
135		iuneq2 4975	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞)) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
137	133, 136	eqtrid 2776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
138	132, 137	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)))
139		ssun2 4142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ {𝑠} ⊆ (ran 𝑓 ∪ {𝑠})
140		vsnid 4627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑠 ∈ {𝑠}
141	139, 140	sselii 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑠 ∈ (ran 𝑓 ∪ {𝑠})
142		elssuni 4901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 ∈ (ran 𝑓 ∪ {𝑠}) → 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
143	141, 142	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑠 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
144		fvssunirn 6891	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓‘𝑞) ⊆ ∪ ran 𝑓
145		ssun1 4141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑠})
146	145	unissi 4880	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ∪ ran 𝑓 ⊆ ∪ (ran 𝑓 ∪ {𝑠})
147	144, 146	sstri 3956	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘𝑞) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
148	143, 147	unssi 4154	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
149	148	rgenw 3048	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
150		iunss 5009	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}) ↔ ∀𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
151	149, 150	mpbir 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ 𝑞 ∈ 𝑑 (𝑠 ∪ (𝑓‘𝑞)) ⊆ ∪ (ran 𝑓 ∪ {𝑠})
152	138, 151	eqsstrdi 3991	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {𝑠}))
153	31	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑎 ⊆ 𝐽)
154	116, 153	sstrd 3957	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ran 𝑓 ⊆ 𝐽)
155	33	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑠 ∈ 𝐽)
156	155	snssd 4773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → {𝑠} ⊆ 𝐽)
157	154, 156	unssd 4155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
158		uniss 4879	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ ∪ 𝐽)
159	158, 2	sseqtrrdi 3988	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
160	157, 159	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∪ (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
161	152, 160	eqssd 3964	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → 𝑋 = ∪ (ran 𝑓 ∪ {𝑠}))
162		unieq 4882	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (ran 𝑓 ∪ {𝑠}) → ∪ 𝑏 = ∪ (ran 𝑓 ∪ {𝑠}))
163	162	rspceeqv 3611	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∪ (ran 𝑓 ∪ {𝑠})) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
164	131, 161, 163	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)
165	164	expr 456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ 𝑑 ∈ Fin) → ((𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
166	165	exlimdv 1933	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) ∧ (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑)) ∧ 𝑑 ∈ Fin) → (∃𝑓(𝑓:𝑑⟶𝑎 ∧ ∀𝑞 ∈ 𝑑 𝑞 = (𝑠 ∪ (𝑓‘𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
167	166	ex 412	. . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → ((𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
171	170	com23 86	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (𝑑 ∈ PtFin → ((𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
172	171	rexlimdv 3132	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝 ∈ 𝑎 ↦ (𝑠 ∪ 𝑝)) ∧ 𝑋 = ∪ 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
173	73, 172	syld 47	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) ∧ (𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))
174	173	rexlimdvaa 3135	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
175	30, 174	syld 47	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
176	175	exlimdv 1933	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (∃𝑥 𝑥 ∈ 𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
177	25, 176	biimtrid 242	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽) → (𝑋 ≠ ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
178	24, 177	pm2.61dne 3011	. . . . . . 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 3131	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → ∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
183	2	iscmp 23275	. . . 4 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
184	183	baibr 536	. . 3 ⊢ (𝐽 ∈ Top → (∀𝑎 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) ↔ 𝐽 ∈ Comp))
185	182, 184	sylibd 239	. 2 ⊢ (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp))
186	14, 185	impbid2 226	1 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3405  Vcvv 3447   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  𝒫 cpw 4563  {csn 4589  ∪ cuni 4871  ∪ ciun 4955   ↦ cmpt 5188  ran crn 5639   Fn wfn 6506  ⟶wf 6507  –onto→wfo 6509  ‘cfv 6511  Fincfn 8918  Topctop 22780  Compccmp 23273  PtFincptfin 23390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-om 7843  df-1o 8434  df-en 8919  df-dom 8920  df-fin 8922  df-top 22781  df-cmp 23274  df-ptfin 23393

This theorem is referenced by: (None)