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

Theorem comppfsc 23524
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 4604 . . . 4 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
2 comppfsc.1 . . . . . . 7 𝑋 = 𝐽
32cmpcov 23381 . . . . . 6 ((𝐽 ∈ Comp ∧ 𝑐𝐽𝑋 = 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
4 elfpw 9391 . . . . . . . 8 (𝑑 ∈ (𝒫 𝑐 ∩ Fin) ↔ (𝑑𝑐𝑑 ∈ Fin))
5 finptfin 23510 . . . . . . . . . . 11 (𝑑 ∈ Fin → 𝑑 ∈ PtFin)
65anim1i 613 . . . . . . . . . 10 ((𝑑 ∈ Fin ∧ (𝑑𝑐𝑋 = 𝑑)) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
76anassrs 466 . . . . . . . . 9 (((𝑑 ∈ Fin ∧ 𝑑𝑐) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
87ancom1s 651 . . . . . . . 8 (((𝑑𝑐𝑑 ∈ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
94, 8sylanb 579 . . . . . . 7 ((𝑑 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
109reximi2 3069 . . . . . 6 (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))
113, 10syl 17 . . . . 5 ((𝐽 ∈ Comp ∧ 𝑐𝐽𝑋 = 𝑐) → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))
12113exp 1116 . . . 4 (𝐽 ∈ Comp → (𝑐𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
131, 12syl5 34 . . 3 (𝐽 ∈ Comp → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
1413ralrimiv 3135 . 2 (𝐽 ∈ Comp → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)))
15 elpwi 4604 . . . . . . 7 (𝑎 ∈ 𝒫 𝐽𝑎𝐽)
16 0elpw 5352 . . . . . . . . . . 11 ∅ ∈ 𝒫 𝑎
17 0fi 9072 . . . . . . . . . . 11 ∅ ∈ Fin
1816, 17elini 4191 . . . . . . . . . 10 ∅ ∈ (𝒫 𝑎 ∩ Fin)
19 unieq 4916 . . . . . . . . . . . 12 (𝑏 = ∅ → 𝑏 = ∅)
20 uni0 4935 . . . . . . . . . . . 12 ∅ = ∅
2119, 20eqtrdi 2782 . . . . . . . . . . 11 (𝑏 = ∅ → 𝑏 = ∅)
2221rspceeqv 3629 . . . . . . . . . 10 ((∅ ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2318, 22mpan 688 . . . . . . . . 9 (𝑋 = ∅ → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2423a1i13 27 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
25 n0 4346 . . . . . . . . 9 (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥𝑋)
26 simp2 1134 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → 𝑋 = 𝑎)
2726eleq2d 2812 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋𝑥 𝑎))
2827biimpd 228 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋𝑥 𝑎))
29 eluni2 4909 . . . . . . . . . . . 12 (𝑥 𝑎 ↔ ∃𝑠𝑎 𝑥𝑠)
3028, 29imbitrdi 250 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋 → ∃𝑠𝑎 𝑥𝑠))
31 simpl3 1190 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑎𝐽)
32 simprl 769 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝑎)
3331, 32sseldd 3979 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝐽)
34 elssuni 4937 . . . . . . . . . . . . . . . . . . . . 21 (𝑠𝐽𝑠 𝐽)
3534, 2sseqtrrdi 4030 . . . . . . . . . . . . . . . . . . . 20 (𝑠𝐽𝑠𝑋)
3633, 35syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝑋)
3736ralrimivw 3140 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑝𝑎 𝑠𝑋)
38 iunss 5045 . . . . . . . . . . . . . . . . . 18 ( 𝑝𝑎 𝑠𝑋 ↔ ∀𝑝𝑎 𝑠𝑋)
3937, 38sylibr 233 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑝𝑎 𝑠𝑋)
40 ssequn1 4178 . . . . . . . . . . . . . . . . 17 ( 𝑝𝑎 𝑠𝑋 ↔ ( 𝑝𝑎 𝑠𝑋) = 𝑋)
4139, 40sylib 217 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ( 𝑝𝑎 𝑠𝑋) = 𝑋)
42 simpl2 1189 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = 𝑎)
43 uniiun 5058 . . . . . . . . . . . . . . . . . 18 𝑎 = 𝑝𝑎 𝑝
4442, 43eqtrdi 2782 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = 𝑝𝑎 𝑝)
4544uneq2d 4160 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ( 𝑝𝑎 𝑠𝑋) = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝))
4641, 45eqtr3d 2768 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝))
47 iunun 5093 . . . . . . . . . . . . . . . 16 𝑝𝑎 (𝑠𝑝) = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝)
48 vex 3466 . . . . . . . . . . . . . . . . . 18 𝑠 ∈ V
49 vex 3466 . . . . . . . . . . . . . . . . . 18 𝑝 ∈ V
5048, 49unex 7746 . . . . . . . . . . . . . . . . 17 (𝑠𝑝) ∈ V
5150dfiun3 5965 . . . . . . . . . . . . . . . 16 𝑝𝑎 (𝑠𝑝) = ran (𝑝𝑎 ↦ (𝑠𝑝))
5247, 51eqtr3i 2756 . . . . . . . . . . . . . . 15 ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝) = ran (𝑝𝑎 ↦ (𝑠𝑝))
5346, 52eqtrdi 2782 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)))
54 simpll1 1209 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝐽 ∈ Top)
5533adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝑠𝐽)
5631sselda 3978 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝑝𝐽)
57 unopn 22893 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ Top ∧ 𝑠𝐽𝑝𝐽) → (𝑠𝑝) ∈ 𝐽)
5854, 55, 56, 57syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → (𝑠𝑝) ∈ 𝐽)
5958fmpttd 7121 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (𝑝𝑎 ↦ (𝑠𝑝)):𝑎𝐽)
6059frnd 6728 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽)
61 elpw2g 5343 . . . . . . . . . . . . . . . . . 18 (𝐽 ∈ Top → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
62613ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
6362adantr 479 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
6460, 63mpbird 256 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽)
65 unieq 4916 . . . . . . . . . . . . . . . . . 18 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → 𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)))
6665eqeq2d 2737 . . . . . . . . . . . . . . . . 17 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (𝑋 = 𝑐𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝))))
67 sseq2 4005 . . . . . . . . . . . . . . . . . . 19 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (𝑑𝑐𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝))))
6867anbi1d 629 . . . . . . . . . . . . . . . . . 18 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ((𝑑𝑐𝑋 = 𝑑) ↔ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
6968rexbidv 3169 . . . . . . . . . . . . . . . . 17 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑) ↔ ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
7066, 69imbi12d 343 . . . . . . . . . . . . . . . 16 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ((𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) ↔ (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7170rspcv 3603 . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥𝑠)
75 ssel2 3973 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝐽𝑠𝑎) → 𝑠𝐽)
76753ad2antl3 1184 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ 𝑠𝑎) → 𝑠𝐽)
7776adantrr 715 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝐽)
78 elunii 4910 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑠𝑠𝐽) → 𝑥 𝐽)
7974, 77, 78syl2anc 582 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥 𝐽)
8079, 2eleqtrrdi 2837 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥𝑋)
8180adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑥𝑋)
82 simprr 771 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑋 = 𝑑)
8381, 82eleqtrd 2828 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑥 𝑑)
84 eqid 2726 . . . . . . . . . . . . . . . . . . . 20 𝑑 = 𝑑
8584ptfinfin 23511 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∈ PtFin ∧ 𝑥 𝑑) → {𝑧𝑑𝑥𝑧} ∈ Fin)
8685expcom 412 . . . . . . . . . . . . . . . . . 18 (𝑥 𝑑 → (𝑑 ∈ PtFin → {𝑧𝑑𝑥𝑧} ∈ Fin))
8783, 86syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ PtFin → {𝑧𝑑𝑥𝑧} ∈ Fin))
88 simprl 769 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)))
89 elun1 4174 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑠𝑥 ∈ (𝑠𝑝))
9089ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥 ∈ (𝑠𝑝))
9190ralrimivw 3140 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝))
9250rgenw 3055 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑝𝑎 (𝑠𝑝) ∈ V
93 eqid 2726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝𝑎 ↦ (𝑠𝑝)) = (𝑝𝑎 ↦ (𝑠𝑝))
94 eleq2 2815 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝑠𝑝) → (𝑥𝑧𝑥 ∈ (𝑠𝑝)))
9593, 94ralrnmptw 7100 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑝𝑎 (𝑠𝑝) ∈ V → (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 ↔ ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝)))
9692, 95ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 ↔ ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝))
9791, 96sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧)
9897adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧)
99 ssralv 4047 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) → (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 → ∀𝑧𝑑 𝑥𝑧))
10088, 98, 99sylc 65 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑧𝑑 𝑥𝑧)
101 rabid2 3453 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = {𝑧𝑑𝑥𝑧} ↔ ∀𝑧𝑑 𝑥𝑧)
102100, 101sylibr 233 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 = {𝑧𝑑𝑥𝑧})
103102eleq1d 2811 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin ↔ {𝑧𝑑𝑥𝑧} ∈ Fin))
104103biimprd 247 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ({𝑧𝑑𝑥𝑧} ∈ Fin → 𝑑 ∈ Fin))
10593rnmpt 5953 . . . . . . . . . . . . . . . . . . . . 21 ran (𝑝𝑎 ↦ (𝑠𝑝)) = {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)}
10688, 105sseqtrdi 4029 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 ⊆ {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)})
107 ssabral 4058 . . . . . . . . . . . . . . . . . . . 20 (𝑑 ⊆ {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)} ↔ ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝))
108106, 107sylib 217 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝))
109 uneq2 4154 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = (𝑓𝑞) → (𝑠𝑝) = (𝑠 ∪ (𝑓𝑞)))
110109eqeq2d 2737 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = (𝑓𝑞) → (𝑞 = (𝑠𝑝) ↔ 𝑞 = (𝑠 ∪ (𝑓𝑞))))
111110ac6sfi 9314 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ Fin ∧ ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝)) → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))
112111expcom 412 . . . . . . . . . . . . . . . . . . 19 (∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))))
113108, 112syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))))
114 frn 6727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑑𝑎 → ran 𝑓𝑎)
115114adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ran 𝑓𝑎)
116115ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓𝑎)
11732ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑠𝑎)
118117snssd 4808 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → {𝑠} ⊆ 𝑎)
119116, 118unssd 4184 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑎)
120 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑑 ∈ Fin)
121 simprrl 779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓:𝑑𝑎)
122121ffnd 6721 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓 Fn 𝑑)
123 dffn4 6813 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn 𝑑𝑓:𝑑onto→ran 𝑓)
124122, 123sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓:𝑑onto→ran 𝑓)
125 fofi 9346 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑑 ∈ Fin ∧ 𝑓:𝑑onto→ran 𝑓) → ran 𝑓 ∈ Fin)
126120, 124, 125syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓 ∈ Fin)
127 snfi 9073 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑠} ∈ Fin
128 unfi 9202 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∈ Fin ∧ {𝑠} ∈ Fin) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
129126, 127, 128sylancl 584 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
130 elfpw 9391 . . . . . . . . . . . . . . . . . . . . . . 23 ((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ↔ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝑎 ∧ (ran 𝑓 ∪ {𝑠}) ∈ Fin))
131119, 129, 130sylanbrc 581 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin))
132 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = 𝑑)
133 uniiun 5058 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑑 = 𝑞𝑑 𝑞
134 simprrr 780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))
135 iuneq2 5012 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)) → 𝑞𝑑 𝑞 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
136134, 135syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑞𝑑 𝑞 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
137133, 136eqtrid 2778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑑 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
138132, 137eqtrd 2766 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
139 ssun2 4171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {𝑠} ⊆ (ran 𝑓 ∪ {𝑠})
140 vsnid 4660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑠 ∈ {𝑠}
141139, 140sselii 3975 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑠 ∈ (ran 𝑓 ∪ {𝑠})
142 elssuni 4937 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ (ran 𝑓 ∪ {𝑠}) → 𝑠 (ran 𝑓 ∪ {𝑠}))
143141, 142ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑠 (ran 𝑓 ∪ {𝑠})
144 fvssunirn 6926 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓𝑞) ⊆ ran 𝑓
145 ssun1 4170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑠})
146145unissi 4914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ran 𝑓 (ran 𝑓 ∪ {𝑠})
147144, 146sstri 3988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝑞) ⊆ (ran 𝑓 ∪ {𝑠})
148143, 147unssi 4183 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
149148rgenw 3055 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
150 iunss 5045 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠}) ↔ ∀𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠}))
151149, 150mpbir 230 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
152138, 151eqsstrdi 4033 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 (ran 𝑓 ∪ {𝑠}))
15331ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑎𝐽)
154116, 153sstrd 3989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓𝐽)
15533ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑠𝐽)
156155snssd 4808 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → {𝑠} ⊆ 𝐽)
157154, 156unssd 4184 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
158 uniss 4913 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
159158, 2sseqtrrdi 4030 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
160157, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
161152, 160eqssd 3996 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = (ran 𝑓 ∪ {𝑠}))
162 unieq 4916 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (ran 𝑓 ∪ {𝑠}) → 𝑏 = (ran 𝑓 ∪ {𝑠}))
163162rspceeqv 3629 . . . . . . . . . . . . . . . . . . . . . 22 (((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = (ran 𝑓 ∪ {𝑠})) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
164131, 161, 163syl2anc 582 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
165164expr 455 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ 𝑑 ∈ Fin) → ((𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
166165exlimdv 1929 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ 𝑑 ∈ Fin) → (∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
167166ex 411 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → (∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
168113, 167mpdd 43 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
16987, 104, 1683syld 60 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
170169ex 411 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ((𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
171170com23 86 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (𝑑 ∈ PtFin → ((𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
172171rexlimdv 3143 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
17373, 172syld 47 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
174173rexlimdvaa 3146 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∃𝑠𝑎 𝑥𝑠 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
17530, 174syld 47 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
176175exlimdv 1929 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∃𝑥 𝑥𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
17725, 176biimtrid 241 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑋 ≠ ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
17824, 177pm2.61dne 3018 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
17915, 178syl3an3 1162 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎 ∈ 𝒫 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
1801793exp 1116 . . . . 5 (𝐽 ∈ Top → (𝑋 = 𝑎 → (𝑎 ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
181180com24 95 . . . 4 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑎 ∈ 𝒫 𝐽 → (𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
182181ralrimdv 3142 . . 3 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
1832iscmp 23380 . . . 4 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
184183baibr 535 . . 3 (𝐽 ∈ Top → (∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) ↔ 𝐽 ∈ Comp))
185182, 184sylibd 238 . 2 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → 𝐽 ∈ Comp))
18614, 185impbid2 225 1 (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wex 1774  wcel 2099  {cab 2703  wne 2930  wral 3051  wrex 3060  {crab 3419  Vcvv 3462  cun 3944  cin 3945  wss 3946  c0 4322  𝒫 cpw 4597  {csn 4623   cuni 4905   ciun 4993  cmpt 5228  ran crn 5675   Fn wfn 6541  wf 6542  ontowfo 6544  cfv 6546  Fincfn 8966  Topctop 22883  Compccmp 23378  PtFincptfin 23495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425  ax-un 7738
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-iun 4995  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-om 7869  df-1o 8488  df-en 8967  df-dom 8968  df-fin 8970  df-top 22884  df-cmp 23379  df-ptfin 23498
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator