Metamath Proof Explorer

Theorem comppfsc

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)

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

Proof

Step Hyp Ref Expression
1 comppfsc.1 ⊢ 𝑋 = ∪ 𝐽
2 elpwi ⊢ ( 𝑐 ∈ 𝒫 𝐽 → 𝑐 ⊆ 𝐽 )
3 1 cmpcov ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 )
4 elfpw ⊢ ( 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) ↔ ( 𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin ) )
5 finptfin ⊢ ( 𝑑 ∈ Fin → 𝑑 ∈ PtFin )
6 5 anim1i ⊢ ( ( 𝑑 ∈ Fin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ PtFin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) )
7 6 anassrs ⊢ ( ( ( 𝑑 ∈ Fin ∧ 𝑑 ⊆ 𝑐 ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ PtFin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) )
8 7 ancom1s ⊢ ( ( ( 𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ PtFin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) )
9 4 8 sylanb ⊢ ( ( 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ PtFin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) )
10 9 reximi2 ⊢ ( ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) )
11 3 10 syl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) )
12 11 3exp ⊢ ( 𝐽 ∈ Comp → ( 𝑐 ⊆ 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) )
13 2 12 syl5 ⊢ ( 𝐽 ∈ Comp → ( 𝑐 ∈ 𝒫 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) )
14 13 ralrimiv ⊢ ( 𝐽 ∈ Comp → ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) )
15 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝐽 → 𝑎 ⊆ 𝐽 )
16 0elpw ⊢ ∅ ∈ 𝒫 𝑎
17 0fin ⊢ ∅ ∈ Fin
18 16 17 elini ⊢ ∅ ∈ ( 𝒫 𝑎 ∩ Fin )
19 unieq ⊢ ( 𝑏 = ∅ → ∪ 𝑏 = ∪ ∅ )
20 uni0 ⊢ ∪ ∅ = ∅
21 19 20 eqtrdi ⊢ ( 𝑏 = ∅ → ∪ 𝑏 = ∅ )
22 21 rspceeqv ⊢ ( ( ∅ ∈ ( 𝒫 𝑎 ∩ Fin ) ∧ 𝑋 = ∅ ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 )
23 18 22 mpan ⊢ ( 𝑋 = ∅ → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 )
24 23 a1i13 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑋 = ∅ → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
25 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑋 )
26 simp2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → 𝑋 = ∪ 𝑎 )
27 26 eleq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑎 ) )
28 27 biimpd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑥 ∈ 𝑋 → 𝑥 ∈ ∪ 𝑎 ) )
29 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝑎 ↔ ∃ 𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 )
30 28 29 syl6ib ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑥 ∈ 𝑋 → ∃ 𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 ) )
31 simpl3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑎 ⊆ 𝐽 )
32 simprl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑠 ∈ 𝑎 )
33 31 32 sseldd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑠 ∈ 𝐽 )
34 elssuni ⊢ ( 𝑠 ∈ 𝐽 → 𝑠 ⊆ ∪ 𝐽 )
35 34 1 sseqtrrdi ⊢ ( 𝑠 ∈ 𝐽 → 𝑠 ⊆ 𝑋 )
36 33 35 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑠 ⊆ 𝑋 )
37 36 ralrimivw ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ∀ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 )
38 iunss ⊢ ( ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ ∀ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 )
39 37 38 sylibr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 )
40 ssequn1 ⊢ ( ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋 ) = 𝑋 )
41 39 40 sylib ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋 ) = 𝑋 )
42 simpl2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑋 = ∪ 𝑎 )
43 uniiun ⊢ ∪ 𝑎 = ∪ 𝑝 ∈ 𝑎 𝑝
44 42 43 eqtrdi ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑋 = ∪ 𝑝 ∈ 𝑎 𝑝 )
45 44 uneq2d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋 ) = ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝 ) )
46 41 45 eqtr3d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑋 = ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝 ) )
47 iunun ⊢ ∪ 𝑝 ∈ 𝑎 ( 𝑠 ∪ 𝑝 ) = ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝 )
48 vex ⊢ 𝑠 ∈ V
49 vex ⊢ 𝑝 ∈ V
50 48 49 unex ⊢ ( 𝑠 ∪ 𝑝 ) ∈ V
51 50 dfiun3 ⊢ ∪ 𝑝 ∈ 𝑎 ( 𝑠 ∪ 𝑝 ) = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) )
52 47 51 eqtr3i ⊢ ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝 ) = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) )
53 46 52 eqtrdi ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) )
54 simpll1 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ 𝑝 ∈ 𝑎 ) → 𝐽 ∈ Top )
55 33 adantr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ 𝑝 ∈ 𝑎 ) → 𝑠 ∈ 𝐽 )
56 31 sselda ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ 𝑝 ∈ 𝑎 ) → 𝑝 ∈ 𝐽 )
57 unopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) → ( 𝑠 ∪ 𝑝 ) ∈ 𝐽 )
58 54 55 56 57 syl3anc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ 𝑝 ∈ 𝑎 ) → ( 𝑠 ∪ 𝑝 ) ∈ 𝐽 )
59 58 fmpttd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) : 𝑎 ⟶ 𝐽 )
60 59 frnd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ⊆ 𝐽 )
61 elpw2g ⊢ ( 𝐽 ∈ Top → ( ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 ↔ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ⊆ 𝐽 ) )
62 61 3ad2ant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 ↔ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ⊆ 𝐽 ) )
63 62 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 ↔ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ⊆ 𝐽 ) )
64 60 63 mpbird ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 )
65 unieq ⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ∪ 𝑐 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) )
66 65 eqeq2d ⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( 𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ) )
67 sseq2 ⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( 𝑑 ⊆ 𝑐 ↔ 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ) )
68 67 anbi1d ⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ↔ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) )
69 68 rexbidv ⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ↔ ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) )
70 66 69 imbi12d ⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ↔ ( 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ) )
71 70 rspcv ⊢ ( ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ) )
72 64 71 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ) )
73 53 72 mpid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) )
74 simprr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ 𝑠 )
75 ssel2 ⊢ ( ( 𝑎 ⊆ 𝐽 ∧ 𝑠 ∈ 𝑎 ) → 𝑠 ∈ 𝐽 )
76 75 3ad2antl3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑠 ∈ 𝑎 ) → 𝑠 ∈ 𝐽 )
77 76 adantrr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑠 ∈ 𝐽 )
78 elunii ⊢ ( ( 𝑥 ∈ 𝑠 ∧ 𝑠 ∈ 𝐽 ) → 𝑥 ∈ ∪ 𝐽 )
79 74 77 78 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ ∪ 𝐽 )
80 79 1 eleqtrrdi ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ 𝑋 )
81 80 adantr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑥 ∈ 𝑋 )
82 simprr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑋 = ∪ 𝑑 )
83 81 82 eleqtrd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑥 ∈ ∪ 𝑑 )
84 eqid ⊢ ∪ 𝑑 = ∪ 𝑑
85 84 ptfinfin ⊢ ( ( 𝑑 ∈ PtFin ∧ 𝑥 ∈ ∪ 𝑑 ) → { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin )
86 85 expcom ⊢ ( 𝑥 ∈ ∪ 𝑑 → ( 𝑑 ∈ PtFin → { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin ) )
87 83 86 syl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ PtFin → { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin ) )
88 simprl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) )
89 elun1 ⊢ ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) )
90 89 ad2antll ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) )
91 90 ralrimivw ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ∀ 𝑝 ∈ 𝑎 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) )
92 50 rgenw ⊢ ∀ 𝑝 ∈ 𝑎 ( 𝑠 ∪ 𝑝 ) ∈ V
93 eqid ⊢ ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) = ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) )
94 eleq2 ⊢ ( 𝑧 = ( 𝑠 ∪ 𝑝 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) ) )
95 93 94 ralrnmptw ⊢ ( ∀ 𝑝 ∈ 𝑎 ( 𝑠 ∪ 𝑝 ) ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 ↔ ∀ 𝑝 ∈ 𝑎 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) ) )
96 92 95 ax-mp ⊢ ( ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 ↔ ∀ 𝑝 ∈ 𝑎 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) )
97 91 96 sylibr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 )
98 97 adantr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 )
99 ssralv ⊢ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 → ∀ 𝑧 ∈ 𝑑 𝑥 ∈ 𝑧 ) )
100 88 98 99 sylc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ∀ 𝑧 ∈ 𝑑 𝑥 ∈ 𝑧 )
101 rabid2 ⊢ ( 𝑑 = { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ↔ ∀ 𝑧 ∈ 𝑑 𝑥 ∈ 𝑧 )
102 100 101 sylibr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑑 = { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } )
103 102 eleq1d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ Fin ↔ { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin ) )
104 103 biimprd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin → 𝑑 ∈ Fin ) )
105 93 rnmpt ⊢ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) = { 𝑞 ∣ ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) }
106 88 105 sseqtrdi ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑑 ⊆ { 𝑞 ∣ ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) } )
107 ssabral ⊢ ( 𝑑 ⊆ { 𝑞 ∣ ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) } ↔ ∀ 𝑞 ∈ 𝑑 ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) )
108 106 107 sylib ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ∀ 𝑞 ∈ 𝑑 ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) )
109 uneq2 ⊢ ( 𝑝 = ( 𝑓 ‘ 𝑞 ) → ( 𝑠 ∪ 𝑝 ) = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) )
110 109 eqeq2d ⊢ ( 𝑝 = ( 𝑓 ‘ 𝑞 ) → ( 𝑞 = ( 𝑠 ∪ 𝑝 ) ↔ 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) )
111 110 ac6sfi ⊢ ( ( 𝑑 ∈ Fin ∧ ∀ 𝑞 ∈ 𝑑 ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) ) → ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) )
112 111 expcom ⊢ ( ∀ 𝑞 ∈ 𝑑 ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) → ( 𝑑 ∈ Fin → ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) )
113 108 112 syl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ Fin → ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) )
114 frn ⊢ ( 𝑓 : 𝑑 ⟶ 𝑎 → ran 𝑓 ⊆ 𝑎 )
115 114 adantr ⊢ ( ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) → ran 𝑓 ⊆ 𝑎 )
116 115 ad2antll ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ran 𝑓 ⊆ 𝑎 )
117 32 ad2antrr ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑠 ∈ 𝑎 )
118 117 snssd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → { 𝑠 } ⊆ 𝑎 )
119 116 118 unssd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝑎 )
120 simprl ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑑 ∈ Fin )
121 simprrl ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑓 : 𝑑 ⟶ 𝑎 )
122 121 ffnd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑓 Fn 𝑑 )
123 dffn4 ⊢ ( 𝑓 Fn 𝑑 ↔ 𝑓 : 𝑑 –onto→ ran 𝑓 )
124 122 123 sylib ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑓 : 𝑑 –onto→ ran 𝑓 )
125 fofi ⊢ ( ( 𝑑 ∈ Fin ∧ 𝑓 : 𝑑 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
126 120 124 125 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ran 𝑓 ∈ Fin )
127 snfi ⊢ { 𝑠 } ∈ Fin
128 unfi ⊢ ( ( ran 𝑓 ∈ Fin ∧ { 𝑠 } ∈ Fin ) → ( ran 𝑓 ∪ { 𝑠 } ) ∈ Fin )
129 126 127 128 sylancl ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ( ran 𝑓 ∪ { 𝑠 } ) ∈ Fin )
130 elfpw ⊢ ( ( ran 𝑓 ∪ { 𝑠 } ) ∈ ( 𝒫 𝑎 ∩ Fin ) ↔ ( ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝑎 ∧ ( ran 𝑓 ∪ { 𝑠 } ) ∈ Fin ) )
131 119 129 130 sylanbrc ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ( ran 𝑓 ∪ { 𝑠 } ) ∈ ( 𝒫 𝑎 ∩ Fin ) )
132 simplrr ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑋 = ∪ 𝑑 )
133 uniiun ⊢ ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 𝑞
134 simprrr ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) )
135 iuneq2 ⊢ ( ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) )
136 134 135 syl ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) )
137 133 136 syl5eq ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) )
138 132 137 eqtrd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑋 = ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) )
139 ssun2 ⊢ { 𝑠 } ⊆ ( ran 𝑓 ∪ { 𝑠 } )
140 vsnid ⊢ 𝑠 ∈ { 𝑠 }
141 139 140 sselii ⊢ 𝑠 ∈ ( ran 𝑓 ∪ { 𝑠 } )
142 elssuni ⊢ ( 𝑠 ∈ ( ran 𝑓 ∪ { 𝑠 } ) → 𝑠 ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) )
143 141 142 ax-mp ⊢ 𝑠 ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } )
144 fvssunirn ⊢ ( 𝑓 ‘ 𝑞 ) ⊆ ∪ ran 𝑓
145 ssun1 ⊢ ran 𝑓 ⊆ ( ran 𝑓 ∪ { 𝑠 } )
146 145 unissi ⊢ ∪ ran 𝑓 ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } )
147 144 146 sstri ⊢ ( 𝑓 ‘ 𝑞 ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } )
148 143 147 unssi ⊢ ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } )
149 148 rgenw ⊢ ∀ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } )
150 iunss ⊢ ( ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) ↔ ∀ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) )
151 149 150 mpbir ⊢ ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } )
152 138 151 eqsstrdi ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) )
153 31 ad2antrr ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑎 ⊆ 𝐽 )
154 116 153 sstrd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ran 𝑓 ⊆ 𝐽 )
155 33 ad2antrr ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑠 ∈ 𝐽 )
156 155 snssd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → { 𝑠 } ⊆ 𝐽 )
157 154 156 unssd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝐽 )
158 uniss ⊢ ( ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝐽 → ∪ ( ran 𝑓 ∪ { 𝑠 } ) ⊆ ∪ 𝐽 )
159 158 1 sseqtrrdi ⊢ ( ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝐽 → ∪ ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝑋 )
160 157 159 syl ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∪ ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝑋 )
161 152 160 eqssd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { 𝑠 } ) )
162 unieq ⊢ ( 𝑏 = ( ran 𝑓 ∪ { 𝑠 } ) → ∪ 𝑏 = ∪ ( ran 𝑓 ∪ { 𝑠 } ) )
163 162 rspceeqv ⊢ ( ( ( ran 𝑓 ∪ { 𝑠 } ) ∈ ( 𝒫 𝑎 ∩ Fin ) ∧ 𝑋 = ∪ ( ran 𝑓 ∪ { 𝑠 } ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 )
164 131 161 163 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 )
165 164 expr ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ 𝑑 ∈ Fin ) → ( ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
166 165 exlimdv ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ 𝑑 ∈ Fin ) → ( ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
167 166 ex ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ Fin → ( ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
168 113 167 mpdd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ Fin → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
169 87 104 168 3syld ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ PtFin → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
170 169 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ PtFin → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
171 170 com23 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( 𝑑 ∈ PtFin → ( ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
172 171 rexlimdv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
173 73 172 syld ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
174 173 rexlimdvaa ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( ∃ 𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
175 30 174 syld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑥 ∈ 𝑋 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
176 175 exlimdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( ∃ 𝑥 𝑥 ∈ 𝑋 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
177 25 176 syl5bi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑋 ≠ ∅ → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
178 24 177 pm2.61dne ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
179 15 178 syl3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ∈ 𝒫 𝐽 ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
180 179 3exp ⊢ ( 𝐽 ∈ Top → ( 𝑋 = ∪ 𝑎 → ( 𝑎 ∈ 𝒫 𝐽 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) )
181 180 com24 ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑎 ∈ 𝒫 𝐽 → ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) )
182 181 ralrimdv ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∀ 𝑎 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
183 1 iscmp ⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑎 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
184 183 baibr ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑎 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ↔ 𝐽 ∈ Comp ) )
185 182 184 sylibd ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → 𝐽 ∈ Comp ) )
186 14 185 impbid2 ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Comp ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) )