MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  comppfsc Structured version   Visualization version   GIF version

Theorem comppfsc 21549
Description: A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
Hypothesis
Ref Expression
comppfsc.1 𝑋 = 𝐽
Assertion
Ref Expression
comppfsc (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
Distinct variable groups:   𝑐,𝑑,𝐽   𝑋,𝑐,𝑑

Proof of Theorem comppfsc
Dummy variables 𝑎 𝑏 𝑓 𝑝 𝑞 𝑠 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elpwi 4361 . . . 4 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
2 comppfsc.1 . . . . . . 7 𝑋 = 𝐽
32cmpcov 21406 . . . . . 6 ((𝐽 ∈ Comp ∧ 𝑐𝐽𝑋 = 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
4 elfpw 8507 . . . . . . . 8 (𝑑 ∈ (𝒫 𝑐 ∩ Fin) ↔ (𝑑𝑐𝑑 ∈ Fin))
5 finptfin 21535 . . . . . . . . . . 11 (𝑑 ∈ Fin → 𝑑 ∈ PtFin)
65anim1i 604 . . . . . . . . . 10 ((𝑑 ∈ Fin ∧ (𝑑𝑐𝑋 = 𝑑)) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
76anassrs 455 . . . . . . . . 9 (((𝑑 ∈ Fin ∧ 𝑑𝑐) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
87ancom1s 635 . . . . . . . 8 (((𝑑𝑐𝑑 ∈ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
94, 8sylanb 572 . . . . . . 7 ((𝑑 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
109reximi2 3197 . . . . . 6 (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))
113, 10syl 17 . . . . 5 ((𝐽 ∈ Comp ∧ 𝑐𝐽𝑋 = 𝑐) → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))
12113exp 1141 . . . 4 (𝐽 ∈ Comp → (𝑐𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
131, 12syl5 34 . . 3 (𝐽 ∈ Comp → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
1413ralrimiv 3153 . 2 (𝐽 ∈ Comp → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)))
15 elpwi 4361 . . . . . . 7 (𝑎 ∈ 𝒫 𝐽𝑎𝐽)
16 0elpw 5026 . . . . . . . . . . . 12 ∅ ∈ 𝒫 𝑎
17 0fin 8427 . . . . . . . . . . . 12 ∅ ∈ Fin
18 elin 3995 . . . . . . . . . . . 12 (∅ ∈ (𝒫 𝑎 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑎 ∧ ∅ ∈ Fin))
1916, 17, 18mpbir2an 693 . . . . . . . . . . 11 ∅ ∈ (𝒫 𝑎 ∩ Fin)
20 unieq 4638 . . . . . . . . . . . . 13 (𝑏 = ∅ → 𝑏 = ∅)
21 uni0 4659 . . . . . . . . . . . . 13 ∅ = ∅
2220, 21syl6eq 2856 . . . . . . . . . . . 12 (𝑏 = ∅ → 𝑏 = ∅)
2322rspceeqv 3520 . . . . . . . . . . 11 ((∅ ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2419, 23mpan 673 . . . . . . . . . 10 (𝑋 = ∅ → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2524a1d 25 . . . . . . . . 9 (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
2625a1i 11 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
27 n0 4132 . . . . . . . . 9 (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥𝑋)
28 simp2 1160 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → 𝑋 = 𝑎)
2928eleq2d 2871 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋𝑥 𝑎))
3029biimpd 220 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋𝑥 𝑎))
31 eluni2 4634 . . . . . . . . . . . 12 (𝑥 𝑎 ↔ ∃𝑠𝑎 𝑥𝑠)
3230, 31syl6ib 242 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋 → ∃𝑠𝑎 𝑥𝑠))
33 simpl3 1239 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑎𝐽)
34 simprl 778 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝑎)
3533, 34sseldd 3799 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝐽)
36 elssuni 4661 . . . . . . . . . . . . . . . . . . . . 21 (𝑠𝐽𝑠 𝐽)
3736, 2syl6sseqr 3849 . . . . . . . . . . . . . . . . . . . 20 (𝑠𝐽𝑠𝑋)
3835, 37syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝑋)
3938ralrimivw 3155 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑝𝑎 𝑠𝑋)
40 iunss 4753 . . . . . . . . . . . . . . . . . 18 ( 𝑝𝑎 𝑠𝑋 ↔ ∀𝑝𝑎 𝑠𝑋)
4139, 40sylibr 225 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑝𝑎 𝑠𝑋)
42 ssequn1 3982 . . . . . . . . . . . . . . . . 17 ( 𝑝𝑎 𝑠𝑋 ↔ ( 𝑝𝑎 𝑠𝑋) = 𝑋)
4341, 42sylib 209 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ( 𝑝𝑎 𝑠𝑋) = 𝑋)
44 simpl2 1237 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = 𝑎)
45 uniiun 4765 . . . . . . . . . . . . . . . . . 18 𝑎 = 𝑝𝑎 𝑝
4644, 45syl6eq 2856 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = 𝑝𝑎 𝑝)
4746uneq2d 3966 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ( 𝑝𝑎 𝑠𝑋) = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝))
4843, 47eqtr3d 2842 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝))
49 iunun 4796 . . . . . . . . . . . . . . . 16 𝑝𝑎 (𝑠𝑝) = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝)
50 vex 3394 . . . . . . . . . . . . . . . . . 18 𝑠 ∈ V
51 vex 3394 . . . . . . . . . . . . . . . . . 18 𝑝 ∈ V
5250, 51unex 7186 . . . . . . . . . . . . . . . . 17 (𝑠𝑝) ∈ V
5352dfiun3 5581 . . . . . . . . . . . . . . . 16 𝑝𝑎 (𝑠𝑝) = ran (𝑝𝑎 ↦ (𝑠𝑝))
5449, 53eqtr3i 2830 . . . . . . . . . . . . . . 15 ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝) = ran (𝑝𝑎 ↦ (𝑠𝑝))
5548, 54syl6eq 2856 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)))
56 simpll1 1262 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝐽 ∈ Top)
5735adantr 468 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝑠𝐽)
5833sselda 3798 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝑝𝐽)
59 unopn 20921 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ Top ∧ 𝑠𝐽𝑝𝐽) → (𝑠𝑝) ∈ 𝐽)
6056, 57, 58, 59syl3anc 1483 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → (𝑠𝑝) ∈ 𝐽)
6160fmpttd 6607 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (𝑝𝑎 ↦ (𝑠𝑝)):𝑎𝐽)
6261frnd 6263 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽)
63 elpw2g 5019 . . . . . . . . . . . . . . . . . 18 (𝐽 ∈ Top → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
64633ad2ant1 1156 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
6564adantr 468 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
6662, 65mpbird 248 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽)
67 unieq 4638 . . . . . . . . . . . . . . . . . 18 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → 𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)))
6867eqeq2d 2816 . . . . . . . . . . . . . . . . 17 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (𝑋 = 𝑐𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝))))
69 sseq2 3824 . . . . . . . . . . . . . . . . . . 19 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (𝑑𝑐𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝))))
7069anbi1d 617 . . . . . . . . . . . . . . . . . 18 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ((𝑑𝑐𝑋 = 𝑑) ↔ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
7170rexbidv 3240 . . . . . . . . . . . . . . . . 17 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑) ↔ ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
7268, 71imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ((𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) ↔ (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7372rspcv 3498 . . . . . . . . . . . . . . 15 (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7466, 73syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7555, 74mpid 44 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
76 simprr 780 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥𝑠)
77 ssel2 3793 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝐽𝑠𝑎) → 𝑠𝐽)
78773ad2antl3 1231 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ 𝑠𝑎) → 𝑠𝐽)
7978adantrr 699 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝐽)
80 elunii 4635 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑠𝑠𝐽) → 𝑥 𝐽)
8176, 79, 80syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥 𝐽)
8281, 2syl6eleqr 2896 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥𝑋)
8382adantr 468 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑥𝑋)
84 simprr 780 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑋 = 𝑑)
8583, 84eleqtrd 2887 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑥 𝑑)
86 eqid 2806 . . . . . . . . . . . . . . . . . . . 20 𝑑 = 𝑑
8786ptfinfin 21536 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∈ PtFin ∧ 𝑥 𝑑) → {𝑧𝑑𝑥𝑧} ∈ Fin)
8887expcom 400 . . . . . . . . . . . . . . . . . 18 (𝑥 𝑑 → (𝑑 ∈ PtFin → {𝑧𝑑𝑥𝑧} ∈ Fin))
8985, 88syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ PtFin → {𝑧𝑑𝑥𝑧} ∈ Fin))
90 simprl 778 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)))
91 elun1 3979 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑠𝑥 ∈ (𝑠𝑝))
9291ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥 ∈ (𝑠𝑝))
9392ralrimivw 3155 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝))
9452rgenw 3112 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑝𝑎 (𝑠𝑝) ∈ V
95 eqid 2806 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝𝑎 ↦ (𝑠𝑝)) = (𝑝𝑎 ↦ (𝑠𝑝))
96 eleq2 2874 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝑠𝑝) → (𝑥𝑧𝑥 ∈ (𝑠𝑝)))
9795, 96ralrnmpt 6590 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑝𝑎 (𝑠𝑝) ∈ V → (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 ↔ ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝)))
9894, 97ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 ↔ ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝))
9993, 98sylibr 225 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧)
10099adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧)
101 ssralv 3863 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) → (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 → ∀𝑧𝑑 𝑥𝑧))
10290, 100, 101sylc 65 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑧𝑑 𝑥𝑧)
103 rabid2 3307 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = {𝑧𝑑𝑥𝑧} ↔ ∀𝑧𝑑 𝑥𝑧)
104102, 103sylibr 225 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 = {𝑧𝑑𝑥𝑧})
105104eleq1d 2870 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin ↔ {𝑧𝑑𝑥𝑧} ∈ Fin))
106105biimprd 239 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ({𝑧𝑑𝑥𝑧} ∈ Fin → 𝑑 ∈ Fin))
10795rnmpt 5572 . . . . . . . . . . . . . . . . . . . . 21 ran (𝑝𝑎 ↦ (𝑠𝑝)) = {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)}
10890, 107syl6sseq 3848 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 ⊆ {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)})
109 ssabral 3870 . . . . . . . . . . . . . . . . . . . 20 (𝑑 ⊆ {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)} ↔ ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝))
110108, 109sylib 209 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝))
111 uneq2 3960 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = (𝑓𝑞) → (𝑠𝑝) = (𝑠 ∪ (𝑓𝑞)))
112111eqeq2d 2816 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = (𝑓𝑞) → (𝑞 = (𝑠𝑝) ↔ 𝑞 = (𝑠 ∪ (𝑓𝑞))))
113112ac6sfi 8443 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ Fin ∧ ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝)) → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))
114113expcom 400 . . . . . . . . . . . . . . . . . . 19 (∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))))
115110, 114syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))))
116 frn 6262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑑𝑎 → ran 𝑓𝑎)
117116adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ran 𝑓𝑎)
118117ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓𝑎)
11934ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑠𝑎)
120119snssd 4530 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → {𝑠} ⊆ 𝑎)
121118, 120unssd 3988 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑎)
122 simprl 778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑑 ∈ Fin)
123 simprrl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓:𝑑𝑎)
124123ffnd 6257 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓 Fn 𝑑)
125 dffn4 6337 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn 𝑑𝑓:𝑑onto→ran 𝑓)
126124, 125sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓:𝑑onto→ran 𝑓)
127 fofi 8491 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑑 ∈ Fin ∧ 𝑓:𝑑onto→ran 𝑓) → ran 𝑓 ∈ Fin)
128122, 126, 127syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓 ∈ Fin)
129 snfi 8277 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑠} ∈ Fin
130 unfi 8466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∈ Fin ∧ {𝑠} ∈ Fin) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
131128, 129, 130sylancl 576 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
132 elfpw 8507 . . . . . . . . . . . . . . . . . . . . . . 23 ((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ↔ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝑎 ∧ (ran 𝑓 ∪ {𝑠}) ∈ Fin))
133121, 131, 132sylanbrc 574 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin))
134 simplrr 787 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = 𝑑)
135 uniiun 4765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑑 = 𝑞𝑑 𝑞
136 simprrr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))
137 iuneq2 4729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)) → 𝑞𝑑 𝑞 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
138136, 137syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑞𝑑 𝑞 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
139135, 138syl5eq 2852 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑑 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
140134, 139eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
141 ssun2 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {𝑠} ⊆ (ran 𝑓 ∪ {𝑠})
142 vsnid 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑠 ∈ {𝑠}
143141, 142sselii 3795 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑠 ∈ (ran 𝑓 ∪ {𝑠})
144 elssuni 4661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ (ran 𝑓 ∪ {𝑠}) → 𝑠 (ran 𝑓 ∪ {𝑠}))
145143, 144ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑠 (ran 𝑓 ∪ {𝑠})
146 fvssunirn 6437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓𝑞) ⊆ ran 𝑓
147 ssun1 3975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑠})
148147unissi 4655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ran 𝑓 (ran 𝑓 ∪ {𝑠})
149146, 148sstri 3807 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝑞) ⊆ (ran 𝑓 ∪ {𝑠})
150145, 149unssi 3987 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
151150rgenw 3112 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
152 iunss 4753 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠}) ↔ ∀𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠}))
153151, 152mpbir 222 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
154140, 153syl6eqss 3852 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 (ran 𝑓 ∪ {𝑠}))
15533ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑎𝐽)
156118, 155sstrd 3808 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓𝐽)
15735ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑠𝐽)
158157snssd 4530 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → {𝑠} ⊆ 𝐽)
159156, 158unssd 3988 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
160 uniss 4653 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
161160, 2syl6sseqr 3849 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
162159, 161syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
163154, 162eqssd 3815 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = (ran 𝑓 ∪ {𝑠}))
164 unieq 4638 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (ran 𝑓 ∪ {𝑠}) → 𝑏 = (ran 𝑓 ∪ {𝑠}))
165164rspceeqv 3520 . . . . . . . . . . . . . . . . . . . . . 22 (((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = (ran 𝑓 ∪ {𝑠})) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
166133, 163, 165syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
167166expr 446 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ 𝑑 ∈ Fin) → ((𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
168167exlimdv 2024 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ 𝑑 ∈ Fin) → (∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
169168ex 399 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → (∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
170115, 169mpdd 43 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
17189, 106, 1703syld 60 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
172171ex 399 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ((𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
173172com23 86 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (𝑑 ∈ PtFin → ((𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
174173rexlimdv 3218 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
17575, 174syld 47 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
176175rexlimdvaa 3220 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∃𝑠𝑎 𝑥𝑠 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
17732, 176syld 47 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
178177exlimdv 2024 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∃𝑥 𝑥𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
17927, 178syl5bi 233 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑋 ≠ ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
18026, 179pm2.61dne 3064 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
18115, 180syl3an3 1198 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎 ∈ 𝒫 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
1821813exp 1141 . . . . 5 (𝐽 ∈ Top → (𝑋 = 𝑎 → (𝑎 ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
183182com24 95 . . . 4 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑎 ∈ 𝒫 𝐽 → (𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
184183ralrimdv 3156 . . 3 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
1852iscmp 21405 . . . 4 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
186185baibr 528 . . 3 (𝐽 ∈ Top → (∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) ↔ 𝐽 ∈ Comp))
187184, 186sylibd 230 . 2 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → 𝐽 ∈ Comp))
18814, 187impbid2 217 1 (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2156  {cab 2792  wne 2978  wral 3096  wrex 3097  {crab 3100  Vcvv 3391  cun 3767  cin 3768  wss 3769  c0 4116  𝒫 cpw 4351  {csn 4370   cuni 4630   ciun 4712  cmpt 4923  ran crn 5312   Fn wfn 6096  wf 6097  ontowfo 6099  cfv 6101  Fincfn 8192  Topctop 20911  Compccmp 21403  PtFincptfin 21520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-oadd 7800  df-er 7979  df-en 8193  df-dom 8194  df-fin 8196  df-top 20912  df-cmp 21404  df-ptfin 21523
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator