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

Theorem comppfsc 22178
 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 4509 . . . 4 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
2 comppfsc.1 . . . . . . 7 𝑋 = 𝐽
32cmpcov 22035 . . . . . 6 ((𝐽 ∈ Comp ∧ 𝑐𝐽𝑋 = 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
4 elfpw 8828 . . . . . . . 8 (𝑑 ∈ (𝒫 𝑐 ∩ Fin) ↔ (𝑑𝑐𝑑 ∈ Fin))
5 finptfin 22164 . . . . . . . . . . 11 (𝑑 ∈ Fin → 𝑑 ∈ PtFin)
65anim1i 617 . . . . . . . . . 10 ((𝑑 ∈ Fin ∧ (𝑑𝑐𝑋 = 𝑑)) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
76anassrs 471 . . . . . . . . 9 (((𝑑 ∈ Fin ∧ 𝑑𝑐) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
87ancom1s 652 . . . . . . . 8 (((𝑑𝑐𝑑 ∈ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
94, 8sylanb 584 . . . . . . 7 ((𝑑 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
109reximi2 3208 . . . . . 6 (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))
113, 10syl 17 . . . . 5 ((𝐽 ∈ Comp ∧ 𝑐𝐽𝑋 = 𝑐) → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))
12113exp 1116 . . . 4 (𝐽 ∈ Comp → (𝑐𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
131, 12syl5 34 . . 3 (𝐽 ∈ Comp → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
1413ralrimiv 3148 . 2 (𝐽 ∈ Comp → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)))
15 elpwi 4509 . . . . . . 7 (𝑎 ∈ 𝒫 𝐽𝑎𝐽)
16 0elpw 5225 . . . . . . . . . . 11 ∅ ∈ 𝒫 𝑎
17 0fin 8748 . . . . . . . . . . 11 ∅ ∈ Fin
1816, 17elini 4123 . . . . . . . . . 10 ∅ ∈ (𝒫 𝑎 ∩ Fin)
19 unieq 4815 . . . . . . . . . . . 12 (𝑏 = ∅ → 𝑏 = ∅)
20 uni0 4832 . . . . . . . . . . . 12 ∅ = ∅
2119, 20eqtrdi 2849 . . . . . . . . . . 11 (𝑏 = ∅ → 𝑏 = ∅)
2221rspceeqv 3587 . . . . . . . . . 10 ((∅ ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2318, 22mpan 689 . . . . . . . . 9 (𝑋 = ∅ → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2423a1i13 27 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
25 n0 4263 . . . . . . . . 9 (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥𝑋)
26 simp2 1134 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → 𝑋 = 𝑎)
2726eleq2d 2875 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋𝑥 𝑎))
2827biimpd 232 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋𝑥 𝑎))
29 eluni2 4808 . . . . . . . . . . . 12 (𝑥 𝑎 ↔ ∃𝑠𝑎 𝑥𝑠)
3028, 29syl6ib 254 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋 → ∃𝑠𝑎 𝑥𝑠))
31 simpl3 1190 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑎𝐽)
32 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝑎)
3331, 32sseldd 3918 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝐽)
34 elssuni 4834 . . . . . . . . . . . . . . . . . . . . 21 (𝑠𝐽𝑠 𝐽)
3534, 2sseqtrrdi 3968 . . . . . . . . . . . . . . . . . . . 20 (𝑠𝐽𝑠𝑋)
3633, 35syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝑋)
3736ralrimivw 3150 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑝𝑎 𝑠𝑋)
38 iunss 4936 . . . . . . . . . . . . . . . . . 18 ( 𝑝𝑎 𝑠𝑋 ↔ ∀𝑝𝑎 𝑠𝑋)
3937, 38sylibr 237 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑝𝑎 𝑠𝑋)
40 ssequn1 4110 . . . . . . . . . . . . . . . . 17 ( 𝑝𝑎 𝑠𝑋 ↔ ( 𝑝𝑎 𝑠𝑋) = 𝑋)
4139, 40sylib 221 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ( 𝑝𝑎 𝑠𝑋) = 𝑋)
42 simpl2 1189 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = 𝑎)
43 uniiun 4949 . . . . . . . . . . . . . . . . . 18 𝑎 = 𝑝𝑎 𝑝
4442, 43eqtrdi 2849 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = 𝑝𝑎 𝑝)
4544uneq2d 4093 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ( 𝑝𝑎 𝑠𝑋) = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝))
4641, 45eqtr3d 2835 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝))
47 iunun 4982 . . . . . . . . . . . . . . . 16 𝑝𝑎 (𝑠𝑝) = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝)
48 vex 3445 . . . . . . . . . . . . . . . . . 18 𝑠 ∈ V
49 vex 3445 . . . . . . . . . . . . . . . . . 18 𝑝 ∈ V
5048, 49unex 7462 . . . . . . . . . . . . . . . . 17 (𝑠𝑝) ∈ V
5150dfiun3 5806 . . . . . . . . . . . . . . . 16 𝑝𝑎 (𝑠𝑝) = ran (𝑝𝑎 ↦ (𝑠𝑝))
5247, 51eqtr3i 2823 . . . . . . . . . . . . . . 15 ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝) = ran (𝑝𝑎 ↦ (𝑠𝑝))
5346, 52eqtrdi 2849 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)))
54 simpll1 1209 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝐽 ∈ Top)
5533adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝑠𝐽)
5631sselda 3917 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝑝𝐽)
57 unopn 21549 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ Top ∧ 𝑠𝐽𝑝𝐽) → (𝑠𝑝) ∈ 𝐽)
5854, 55, 56, 57syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → (𝑠𝑝) ∈ 𝐽)
5958fmpttd 6866 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (𝑝𝑎 ↦ (𝑠𝑝)):𝑎𝐽)
6059frnd 6502 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽)
61 elpw2g 5215 . . . . . . . . . . . . . . . . . 18 (𝐽 ∈ Top → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
62613ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
6362adantr 484 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
6460, 63mpbird 260 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽)
65 unieq 4815 . . . . . . . . . . . . . . . . . 18 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → 𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)))
6665eqeq2d 2809 . . . . . . . . . . . . . . . . 17 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (𝑋 = 𝑐𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝))))
67 sseq2 3943 . . . . . . . . . . . . . . . . . . 19 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (𝑑𝑐𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝))))
6867anbi1d 632 . . . . . . . . . . . . . . . . . 18 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ((𝑑𝑐𝑋 = 𝑑) ↔ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
6968rexbidv 3257 . . . . . . . . . . . . . . . . 17 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑) ↔ ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
7066, 69imbi12d 348 . . . . . . . . . . . . . . . 16 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ((𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) ↔ (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7170rspcv 3567 . . . . . . . . . . . . . . 15 (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7264, 71syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7353, 72mpid 44 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
74 simprr 772 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥𝑠)
75 ssel2 3912 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝐽𝑠𝑎) → 𝑠𝐽)
76753ad2antl3 1184 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ 𝑠𝑎) → 𝑠𝐽)
7776adantrr 716 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝐽)
78 elunii 4809 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑠𝑠𝐽) → 𝑥 𝐽)
7974, 77, 78syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥 𝐽)
8079, 2eleqtrrdi 2901 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥𝑋)
8180adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑥𝑋)
82 simprr 772 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑋 = 𝑑)
8381, 82eleqtrd 2892 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑥 𝑑)
84 eqid 2798 . . . . . . . . . . . . . . . . . . . 20 𝑑 = 𝑑
8584ptfinfin 22165 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∈ PtFin ∧ 𝑥 𝑑) → {𝑧𝑑𝑥𝑧} ∈ Fin)
8685expcom 417 . . . . . . . . . . . . . . . . . 18 (𝑥 𝑑 → (𝑑 ∈ PtFin → {𝑧𝑑𝑥𝑧} ∈ Fin))
8783, 86syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ PtFin → {𝑧𝑑𝑥𝑧} ∈ Fin))
88 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)))
89 elun1 4106 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑠𝑥 ∈ (𝑠𝑝))
9089ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥 ∈ (𝑠𝑝))
9190ralrimivw 3150 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝))
9250rgenw 3118 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑝𝑎 (𝑠𝑝) ∈ V
93 eqid 2798 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝𝑎 ↦ (𝑠𝑝)) = (𝑝𝑎 ↦ (𝑠𝑝))
94 eleq2 2878 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝑠𝑝) → (𝑥𝑧𝑥 ∈ (𝑠𝑝)))
9593, 94ralrnmptw 6847 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑝𝑎 (𝑠𝑝) ∈ V → (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 ↔ ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝)))
9692, 95ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 ↔ ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝))
9791, 96sylibr 237 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧)
9897adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧)
99 ssralv 3983 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) → (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 → ∀𝑧𝑑 𝑥𝑧))
10088, 98, 99sylc 65 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑧𝑑 𝑥𝑧)
101 rabid2 3335 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = {𝑧𝑑𝑥𝑧} ↔ ∀𝑧𝑑 𝑥𝑧)
102100, 101sylibr 237 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 = {𝑧𝑑𝑥𝑧})
103102eleq1d 2874 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin ↔ {𝑧𝑑𝑥𝑧} ∈ Fin))
104103biimprd 251 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ({𝑧𝑑𝑥𝑧} ∈ Fin → 𝑑 ∈ Fin))
10593rnmpt 5795 . . . . . . . . . . . . . . . . . . . . 21 ran (𝑝𝑎 ↦ (𝑠𝑝)) = {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)}
10688, 105sseqtrdi 3967 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 ⊆ {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)})
107 ssabral 3992 . . . . . . . . . . . . . . . . . . . 20 (𝑑 ⊆ {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)} ↔ ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝))
108106, 107sylib 221 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝))
109 uneq2 4087 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = (𝑓𝑞) → (𝑠𝑝) = (𝑠 ∪ (𝑓𝑞)))
110109eqeq2d 2809 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = (𝑓𝑞) → (𝑞 = (𝑠𝑝) ↔ 𝑞 = (𝑠 ∪ (𝑓𝑞))))
111110ac6sfi 8764 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ Fin ∧ ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝)) → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))
112111expcom 417 . . . . . . . . . . . . . . . . . . 19 (∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))))
113108, 112syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))))
114 frn 6501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑑𝑎 → ran 𝑓𝑎)
115114adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ran 𝑓𝑎)
116115ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓𝑎)
11732ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑠𝑎)
118117snssd 4705 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → {𝑠} ⊆ 𝑎)
119116, 118unssd 4116 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑎)
120 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑑 ∈ Fin)
121 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓:𝑑𝑎)
122121ffnd 6496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓 Fn 𝑑)
123 dffn4 6579 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn 𝑑𝑓:𝑑onto→ran 𝑓)
124122, 123sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓:𝑑onto→ran 𝑓)
125 fofi 8812 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑑 ∈ Fin ∧ 𝑓:𝑑onto→ran 𝑓) → ran 𝑓 ∈ Fin)
126120, 124, 125syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓 ∈ Fin)
127 snfi 8595 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑠} ∈ Fin
128 unfi 8787 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∈ Fin ∧ {𝑠} ∈ Fin) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
129126, 127, 128sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
130 elfpw 8828 . . . . . . . . . . . . . . . . . . . . . . 23 ((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ↔ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝑎 ∧ (ran 𝑓 ∪ {𝑠}) ∈ Fin))
131119, 129, 130sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin))
132 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = 𝑑)
133 uniiun 4949 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑑 = 𝑞𝑑 𝑞
134 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))
135 iuneq2 4904 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)) → 𝑞𝑑 𝑞 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
136134, 135syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑞𝑑 𝑞 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
137133, 136syl5eq 2845 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑑 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
138132, 137eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
139 ssun2 4103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {𝑠} ⊆ (ran 𝑓 ∪ {𝑠})
140 vsnid 4565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑠 ∈ {𝑠}
141139, 140sselii 3914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑠 ∈ (ran 𝑓 ∪ {𝑠})
142 elssuni 4834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ (ran 𝑓 ∪ {𝑠}) → 𝑠 (ran 𝑓 ∪ {𝑠}))
143141, 142ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑠 (ran 𝑓 ∪ {𝑠})
144 fvssunirn 6684 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓𝑞) ⊆ ran 𝑓
145 ssun1 4102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑠})
146145unissi 4813 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ran 𝑓 (ran 𝑓 ∪ {𝑠})
147144, 146sstri 3926 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝑞) ⊆ (ran 𝑓 ∪ {𝑠})
148143, 147unssi 4115 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
149148rgenw 3118 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
150 iunss 4936 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠}) ↔ ∀𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠}))
151149, 150mpbir 234 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
152138, 151eqsstrdi 3971 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 (ran 𝑓 ∪ {𝑠}))
15331ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑎𝐽)
154116, 153sstrd 3927 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓𝐽)
15533ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑠𝐽)
156155snssd 4705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → {𝑠} ⊆ 𝐽)
157154, 156unssd 4116 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
158 uniss 4812 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
159158, 2sseqtrrdi 3968 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
160157, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
161152, 160eqssd 3934 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = (ran 𝑓 ∪ {𝑠}))
162 unieq 4815 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (ran 𝑓 ∪ {𝑠}) → 𝑏 = (ran 𝑓 ∪ {𝑠}))
163162rspceeqv 3587 . . . . . . . . . . . . . . . . . . . . . 22 (((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = (ran 𝑓 ∪ {𝑠})) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
164131, 161, 163syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
165164expr 460 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ 𝑑 ∈ Fin) → ((𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
166165exlimdv 1934 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ 𝑑 ∈ Fin) → (∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
167166ex 416 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → (∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
168113, 167mpdd 43 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
16987, 104, 1683syld 60 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
170169ex 416 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ((𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
171170com23 86 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (𝑑 ∈ PtFin → ((𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
172171rexlimdv 3243 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
17373, 172syld 47 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
174173rexlimdvaa 3245 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∃𝑠𝑎 𝑥𝑠 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
17530, 174syld 47 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
176175exlimdv 1934 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∃𝑥 𝑥𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
17725, 176syl5bi 245 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑋 ≠ ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
17824, 177pm2.61dne 3073 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
17915, 178syl3an3 1162 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎 ∈ 𝒫 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
1801793exp 1116 . . . . 5 (𝐽 ∈ Top → (𝑋 = 𝑎 → (𝑎 ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
181180com24 95 . . . 4 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑎 ∈ 𝒫 𝐽 → (𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
182181ralrimdv 3153 . . 3 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
1832iscmp 22034 . . . 4 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
184183baibr 540 . . 3 (𝐽 ∈ Top → (∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) ↔ 𝐽 ∈ Comp))
185182, 184sylibd 242 . 2 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → 𝐽 ∈ Comp))
18614, 185impbid2 229 1 (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3442   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4246  𝒫 cpw 4500  {csn 4528  ∪ cuni 4804  ∪ ciun 4885   ↦ cmpt 5114  ran crn 5524   Fn wfn 6327  ⟶wf 6328  –onto→wfo 6330  ‘cfv 6332  Fincfn 8510  Topctop 21539  Compccmp 22032  PtFincptfin 22149 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-oadd 8107  df-er 8290  df-en 8511  df-dom 8512  df-fin 8514  df-top 21540  df-cmp 22033  df-ptfin 22152 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator