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

Theorem comppfsc 21087
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 4116 . . . 4 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
2 comppfsc.1 . . . . . . 7 𝑋 = 𝐽
32cmpcov 20944 . . . . . 6 ((𝐽 ∈ Comp ∧ 𝑐𝐽𝑋 = 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
4 elfpw 8128 . . . . . . . 8 (𝑑 ∈ (𝒫 𝑐 ∩ Fin) ↔ (𝑑𝑐𝑑 ∈ Fin))
5 finptfin 21073 . . . . . . . . . . 11 (𝑑 ∈ Fin → 𝑑 ∈ PtFin)
65anim1i 589 . . . . . . . . . 10 ((𝑑 ∈ Fin ∧ (𝑑𝑐𝑋 = 𝑑)) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
76anassrs 677 . . . . . . . . 9 (((𝑑 ∈ Fin ∧ 𝑑𝑐) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
87ancom1s 842 . . . . . . . 8 (((𝑑𝑐𝑑 ∈ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
94, 8sylanb 487 . . . . . . 7 ((𝑑 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin ∧ (𝑑𝑐𝑋 = 𝑑)))
109reximi2 2992 . . . . . 6 (∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))
113, 10syl 17 . . . . 5 ((𝐽 ∈ Comp ∧ 𝑐𝐽𝑋 = 𝑐) → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))
12113exp 1255 . . . 4 (𝐽 ∈ Comp → (𝑐𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
131, 12syl5 33 . . 3 (𝐽 ∈ Comp → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
1413ralrimiv 2947 . 2 (𝐽 ∈ Comp → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)))
15 elpwi 4116 . . . . . . 7 (𝑎 ∈ 𝒫 𝐽𝑎𝐽)
16 0elpw 4755 . . . . . . . . . . . 12 ∅ ∈ 𝒫 𝑎
17 0fin 8050 . . . . . . . . . . . 12 ∅ ∈ Fin
18 elin 3757 . . . . . . . . . . . 12 (∅ ∈ (𝒫 𝑎 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑎 ∧ ∅ ∈ Fin))
1916, 17, 18mpbir2an 956 . . . . . . . . . . 11 ∅ ∈ (𝒫 𝑎 ∩ Fin)
20 unieq 4374 . . . . . . . . . . . . . 14 (𝑏 = ∅ → 𝑏 = ∅)
21 uni0 4395 . . . . . . . . . . . . . 14 ∅ = ∅
2220, 21syl6eq 2659 . . . . . . . . . . . . 13 (𝑏 = ∅ → 𝑏 = ∅)
2322eqeq2d 2619 . . . . . . . . . . . 12 (𝑏 = ∅ → (𝑋 = 𝑏𝑋 = ∅))
2423rspcev 3281 . . . . . . . . . . 11 ((∅ ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2519, 24mpan 701 . . . . . . . . . 10 (𝑋 = ∅ → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
2625a1d 25 . . . . . . . . 9 (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
2726a1i 11 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑋 = ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
28 n0 3889 . . . . . . . . 9 (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥𝑋)
29 simp2 1054 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → 𝑋 = 𝑎)
3029eleq2d 2672 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋𝑥 𝑎))
3130biimpd 217 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋𝑥 𝑎))
32 eluni2 4370 . . . . . . . . . . . 12 (𝑥 𝑎 ↔ ∃𝑠𝑎 𝑥𝑠)
3331, 32syl6ib 239 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋 → ∃𝑠𝑎 𝑥𝑠))
34 simpl3 1058 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑎𝐽)
35 simprl 789 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝑎)
3634, 35sseldd 3568 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝐽)
37 elssuni 4397 . . . . . . . . . . . . . . . . . . . . 21 (𝑠𝐽𝑠 𝐽)
3837, 2syl6sseqr 3614 . . . . . . . . . . . . . . . . . . . 20 (𝑠𝐽𝑠𝑋)
3936, 38syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝑋)
4039ralrimivw 2949 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑝𝑎 𝑠𝑋)
41 iunss 4491 . . . . . . . . . . . . . . . . . 18 ( 𝑝𝑎 𝑠𝑋 ↔ ∀𝑝𝑎 𝑠𝑋)
4240, 41sylibr 222 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑝𝑎 𝑠𝑋)
43 ssequn1 3744 . . . . . . . . . . . . . . . . 17 ( 𝑝𝑎 𝑠𝑋 ↔ ( 𝑝𝑎 𝑠𝑋) = 𝑋)
4442, 43sylib 206 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ( 𝑝𝑎 𝑠𝑋) = 𝑋)
45 simpl2 1057 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = 𝑎)
46 uniiun 4503 . . . . . . . . . . . . . . . . . 18 𝑎 = 𝑝𝑎 𝑝
4745, 46syl6eq 2659 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = 𝑝𝑎 𝑝)
4847uneq2d 3728 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ( 𝑝𝑎 𝑠𝑋) = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝))
4944, 48eqtr3d 2645 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝))
50 iunun 4534 . . . . . . . . . . . . . . . 16 𝑝𝑎 (𝑠𝑝) = ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝)
51 vex 3175 . . . . . . . . . . . . . . . . . 18 𝑠 ∈ V
52 vex 3175 . . . . . . . . . . . . . . . . . 18 𝑝 ∈ V
5351, 52unex 6831 . . . . . . . . . . . . . . . . 17 (𝑠𝑝) ∈ V
5453dfiun3 5288 . . . . . . . . . . . . . . . 16 𝑝𝑎 (𝑠𝑝) = ran (𝑝𝑎 ↦ (𝑠𝑝))
5550, 54eqtr3i 2633 . . . . . . . . . . . . . . 15 ( 𝑝𝑎 𝑠 𝑝𝑎 𝑝) = ran (𝑝𝑎 ↦ (𝑠𝑝))
5649, 55syl6eq 2659 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)))
57 simpll1 1092 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝐽 ∈ Top)
5836adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝑠𝐽)
5934sselda 3567 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → 𝑝𝐽)
60 unopn 20475 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ Top ∧ 𝑠𝐽𝑝𝐽) → (𝑠𝑝) ∈ 𝐽)
6157, 58, 59, 60syl3anc 1317 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ 𝑝𝑎) → (𝑠𝑝) ∈ 𝐽)
62 eqid 2609 . . . . . . . . . . . . . . . . . 18 (𝑝𝑎 ↦ (𝑠𝑝)) = (𝑝𝑎 ↦ (𝑠𝑝))
6361, 62fmptd 6277 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (𝑝𝑎 ↦ (𝑠𝑝)):𝑎𝐽)
64 frn 5952 . . . . . . . . . . . . . . . . 17 ((𝑝𝑎 ↦ (𝑠𝑝)):𝑎𝐽 → ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽)
6563, 64syl 17 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽)
66 elpw2g 4749 . . . . . . . . . . . . . . . . . 18 (𝐽 ∈ Top → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
67663ad2ant1 1074 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
6867adantr 479 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 ↔ ran (𝑝𝑎 ↦ (𝑠𝑝)) ⊆ 𝐽))
6965, 68mpbird 245 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽)
70 unieq 4374 . . . . . . . . . . . . . . . . . 18 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → 𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)))
7170eqeq2d 2619 . . . . . . . . . . . . . . . . 17 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (𝑋 = 𝑐𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝))))
72 sseq2 3589 . . . . . . . . . . . . . . . . . . 19 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (𝑑𝑐𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝))))
7372anbi1d 736 . . . . . . . . . . . . . . . . . 18 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ((𝑑𝑐𝑋 = 𝑑) ↔ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
7473rexbidv 3033 . . . . . . . . . . . . . . . . 17 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → (∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑) ↔ ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
7571, 74imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑐 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ((𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) ↔ (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7675rspcv 3277 . . . . . . . . . . . . . . 15 (ran (𝑝𝑎 ↦ (𝑠𝑝)) ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7769, 76syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑋 = ran (𝑝𝑎 ↦ (𝑠𝑝)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑))))
7856, 77mpid 42 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)))
79 simprr 791 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥𝑠)
80 ssel2 3562 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝐽𝑠𝑎) → 𝑠𝐽)
81803ad2antl3 1217 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ 𝑠𝑎) → 𝑠𝐽)
8281adantrr 748 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑠𝐽)
83 elunii 4371 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑠𝑠𝐽) → 𝑥 𝐽)
8479, 82, 83syl2anc 690 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥 𝐽)
8584, 2syl6eleqr 2698 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥𝑋)
8685adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑥𝑋)
87 simprr 791 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑋 = 𝑑)
8886, 87eleqtrd 2689 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑥 𝑑)
89 eqid 2609 . . . . . . . . . . . . . . . . . . . 20 𝑑 = 𝑑
9089ptfinfin 21074 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∈ PtFin ∧ 𝑥 𝑑) → {𝑧𝑑𝑥𝑧} ∈ Fin)
9190expcom 449 . . . . . . . . . . . . . . . . . 18 (𝑥 𝑑 → (𝑑 ∈ PtFin → {𝑧𝑑𝑥𝑧} ∈ Fin))
9288, 91syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ PtFin → {𝑧𝑑𝑥𝑧} ∈ Fin))
93 simprl 789 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)))
94 elun1 3741 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑠𝑥 ∈ (𝑠𝑝))
9594ad2antll 760 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → 𝑥 ∈ (𝑠𝑝))
9695ralrimivw 2949 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝))
9753rgenw 2907 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑝𝑎 (𝑠𝑝) ∈ V
98 eleq2 2676 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = (𝑠𝑝) → (𝑥𝑧𝑥 ∈ (𝑠𝑝)))
9962, 98ralrnmpt 6261 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑝𝑎 (𝑠𝑝) ∈ V → (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 ↔ ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝)))
10097, 99ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 ↔ ∀𝑝𝑎 𝑥 ∈ (𝑠𝑝))
10196, 100sylibr 222 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧)
102101adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧)
103 ssralv 3628 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) → (∀𝑧 ∈ ran (𝑝𝑎 ↦ (𝑠𝑝))𝑥𝑧 → ∀𝑧𝑑 𝑥𝑧))
10493, 102, 103sylc 62 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑧𝑑 𝑥𝑧)
105 rabid2 3095 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = {𝑧𝑑𝑥𝑧} ↔ ∀𝑧𝑑 𝑥𝑧)
106104, 105sylibr 222 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 = {𝑧𝑑𝑥𝑧})
107106eleq1d 2671 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin ↔ {𝑧𝑑𝑥𝑧} ∈ Fin))
108107biimprd 236 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ({𝑧𝑑𝑥𝑧} ∈ Fin → 𝑑 ∈ Fin))
10962rnmpt 5279 . . . . . . . . . . . . . . . . . . . . 21 ran (𝑝𝑎 ↦ (𝑠𝑝)) = {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)}
11093, 109syl6sseq 3613 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → 𝑑 ⊆ {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)})
111 ssabral 3635 . . . . . . . . . . . . . . . . . . . 20 (𝑑 ⊆ {𝑞 ∣ ∃𝑝𝑎 𝑞 = (𝑠𝑝)} ↔ ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝))
112110, 111sylib 206 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝))
113 uneq2 3722 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 = (𝑓𝑞) → (𝑠𝑝) = (𝑠 ∪ (𝑓𝑞)))
114113eqeq2d 2619 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = (𝑓𝑞) → (𝑞 = (𝑠𝑝) ↔ 𝑞 = (𝑠 ∪ (𝑓𝑞))))
115114ac6sfi 8066 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ Fin ∧ ∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝)) → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))
116115expcom 449 . . . . . . . . . . . . . . . . . . 19 (∀𝑞𝑑𝑝𝑎 𝑞 = (𝑠𝑝) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))))
117112, 116syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → ∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))))
118 frn 5952 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓:𝑑𝑎 → ran 𝑓𝑎)
119118adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ran 𝑓𝑎)
120119ad2antll 760 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓𝑎)
12135ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑠𝑎)
122121snssd 4280 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → {𝑠} ⊆ 𝑎)
123120, 122unssd 3750 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑎)
124 simprl 789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑑 ∈ Fin)
125 simprrl 799 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓:𝑑𝑎)
126 ffn 5944 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓:𝑑𝑎𝑓 Fn 𝑑)
127125, 126syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓 Fn 𝑑)
128 dffn4 6019 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 Fn 𝑑𝑓:𝑑onto→ran 𝑓)
129127, 128sylib 206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑓:𝑑onto→ran 𝑓)
130 fofi 8112 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑑 ∈ Fin ∧ 𝑓:𝑑onto→ran 𝑓) → ran 𝑓 ∈ Fin)
131124, 129, 130syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓 ∈ Fin)
132 snfi 7900 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑠} ∈ Fin
133 unfi 8089 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∈ Fin ∧ {𝑠} ∈ Fin) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
134131, 132, 133sylancl 692 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ Fin)
135 elfpw 8128 . . . . . . . . . . . . . . . . . . . . . . 23 ((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ↔ ((ran 𝑓 ∪ {𝑠}) ⊆ 𝑎 ∧ (ran 𝑓 ∪ {𝑠}) ∈ Fin))
136123, 134, 135sylanbrc 694 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin))
137 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = 𝑑)
138 uniiun 4503 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑑 = 𝑞𝑑 𝑞
139 simprrr 800 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)))
140 iuneq2 4467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞)) → 𝑞𝑑 𝑞 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
141139, 140syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑞𝑑 𝑞 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
142138, 141syl5eq 2655 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑑 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
143137, 142eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)))
144 ssun2 3738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {𝑠} ⊆ (ran 𝑓 ∪ {𝑠})
145 vsnid 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑠 ∈ {𝑠}
146144, 145sselii 3564 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑠 ∈ (ran 𝑓 ∪ {𝑠})
147 elssuni 4397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 ∈ (ran 𝑓 ∪ {𝑠}) → 𝑠 (ran 𝑓 ∪ {𝑠}))
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑠 (ran 𝑓 ∪ {𝑠})
149 fvssunirn 6112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓𝑞) ⊆ ran 𝑓
150 ssun1 3737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ran 𝑓 ⊆ (ran 𝑓 ∪ {𝑠})
151150unissi 4391 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ran 𝑓 (ran 𝑓 ∪ {𝑠})
152149, 151sstri 3576 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝑞) ⊆ (ran 𝑓 ∪ {𝑠})
153148, 152unssi 3749 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
154153rgenw 2907 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
155 iunss 4491 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠}) ↔ ∀𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠}))
156154, 155mpbir 219 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑞𝑑 (𝑠 ∪ (𝑓𝑞)) ⊆ (ran 𝑓 ∪ {𝑠})
157143, 156syl6eqss 3617 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 (ran 𝑓 ∪ {𝑠}))
15834ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑎𝐽)
159120, 158sstrd 3577 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ran 𝑓𝐽)
16036ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑠𝐽)
161160snssd 4280 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → {𝑠} ⊆ 𝐽)
162159, 161unssd 3750 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
163 uniss 4388 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 (ran 𝑓 ∪ {𝑠}) ⊆ 𝐽)
164163, 2syl6sseqr 3614 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ran 𝑓 ∪ {𝑠}) ⊆ 𝐽 (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
165162, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → (ran 𝑓 ∪ {𝑠}) ⊆ 𝑋)
166157, 165eqssd 3584 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → 𝑋 = (ran 𝑓 ∪ {𝑠}))
167 unieq 4374 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = (ran 𝑓 ∪ {𝑠}) → 𝑏 = (ran 𝑓 ∪ {𝑠}))
168167eqeq2d 2619 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (ran 𝑓 ∪ {𝑠}) → (𝑋 = 𝑏𝑋 = (ran 𝑓 ∪ {𝑠})))
169168rspcev 3281 . . . . . . . . . . . . . . . . . . . . . 22 (((ran 𝑓 ∪ {𝑠}) ∈ (𝒫 𝑎 ∩ Fin) ∧ 𝑋 = (ran 𝑓 ∪ {𝑠})) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
170136, 166, 169syl2anc 690 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ (𝑑 ∈ Fin ∧ (𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)
171170expr 640 . . . . . . . . . . . . . . . . . . . 20 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ 𝑑 ∈ Fin) → ((𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
172171exlimdv 1847 . . . . . . . . . . . . . . . . . . 19 (((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) ∧ 𝑑 ∈ Fin) → (∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
173172ex 448 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → (∃𝑓(𝑓:𝑑𝑎 ∧ ∀𝑞𝑑 𝑞 = (𝑠 ∪ (𝑓𝑞))) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
174117, 173mpdd 41 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ Fin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
17592, 108, 1743syld 57 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) ∧ (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑)) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
176175ex 448 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → ((𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → (𝑑 ∈ PtFin → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
177176com23 83 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (𝑑 ∈ PtFin → ((𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
178177rexlimdv 3011 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∃𝑑 ∈ PtFin (𝑑 ⊆ ran (𝑝𝑎 ↦ (𝑠𝑝)) ∧ 𝑋 = 𝑑) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
17978, 178syld 45 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) ∧ (𝑠𝑎𝑥𝑠)) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
180179rexlimdvaa 3013 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∃𝑠𝑎 𝑥𝑠 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
18133, 180syld 45 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑥𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
182181exlimdv 1847 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∃𝑥 𝑥𝑋 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
18328, 182syl5bi 230 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (𝑋 ≠ ∅ → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
18427, 183pm2.61dne 2867 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
18515, 184syl3an3 1352 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑋 = 𝑎𝑎 ∈ 𝒫 𝐽) → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))
1861853exp 1255 . . . . 5 (𝐽 ∈ Top → (𝑋 = 𝑎 → (𝑎 ∈ 𝒫 𝐽 → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
187186com24 92 . . . 4 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → (𝑎 ∈ 𝒫 𝐽 → (𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏))))
188187ralrimdv 2950 . . 3 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → ∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
1892iscmp 20943 . . . 4 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏)))
190189baibr 942 . . 3 (𝐽 ∈ Top → (∀𝑎 ∈ 𝒫 𝐽(𝑋 = 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = 𝑏) ↔ 𝐽 ∈ Comp))
191188, 190sylibd 227 . 2 (𝐽 ∈ Top → (∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑)) → 𝐽 ∈ Comp))
19214, 191impbid2 214 1 (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ PtFin (𝑑𝑐𝑋 = 𝑑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1976  {cab 2595  wne 2779  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  cun 3537  cin 3538  wss 3539  c0 3873  𝒫 cpw 4107  {csn 4124   cuni 4366   ciun 4449  cmpt 4637  ran crn 5029   Fn wfn 5785  wf 5786  ontowfo 5788  cfv 5790  Fincfn 7818  Topctop 20459  Compccmp 20941  PtFincptfin 21058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-en 7819  df-dom 7820  df-fin 7822  df-top 20463  df-cmp 20942  df-ptfin 21061
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator