ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnptopco GIF version
Theorem cnptopco 13807
Description: The composition of a function 𝐹 continuous at 𝑃 with a function continuous at (πΉβ€˜π‘ƒ) is continuous at 𝑃. Proposition 2 of [BourbakiTop1] p. I.9. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
Assertion
Ref Expression
cnptopco (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ (𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)β€˜π‘ƒ))
Proof of Theorem cnptopco
Dummy variables π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl2 1001 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐾 ∈ Top)
2 toptopon2 13604 . . . . 5 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
31, 2sylib 122 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
4 simpl3 1002 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐿 ∈ Top)
5 toptopon2 13604 . . . . 5 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
64, 5sylib 122 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
7 simprr 531 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))
8 cnpf2 13792 . . . 4 ((𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾) ∧ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ))) β†’ 𝐺:βˆͺ 𝐾⟢βˆͺ 𝐿)
93, 6, 7, 8syl3anc 1238 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐺:βˆͺ 𝐾⟢βˆͺ 𝐿)
10 simpl1 1000 . . . . 5 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐽 ∈ Top)
11 toptopon2 13604 . . . . 5 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽))
1210, 11sylib 122 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽))
13 simprl 529 . . . 4 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ))
14 cnpf2 13792 . . . 4 ((𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ 𝐹:βˆͺ 𝐽⟢βˆͺ 𝐾)
1512, 3, 13, 14syl3anc 1238 . . 3 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝐹:βˆͺ 𝐽⟢βˆͺ 𝐾)
16 fco 5383 . . 3 ((𝐺:βˆͺ 𝐾⟢βˆͺ 𝐿 ∧ 𝐹:βˆͺ 𝐽⟢βˆͺ 𝐾) β†’ (𝐺 ∘ 𝐹):βˆͺ 𝐽⟢βˆͺ 𝐿)
179, 15, 16syl2anc 411 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ (𝐺 ∘ 𝐹):βˆͺ 𝐽⟢βˆͺ 𝐿)
183adantr 276 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
196adantr 276 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿))
20 cnprcl2k 13791 . . . . . . . . 9 ((𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽) ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ 𝑃 ∈ βˆͺ 𝐽)
2112, 1, 13, 20syl3anc 1238 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ 𝑃 ∈ βˆͺ 𝐽)
2215, 21ffvelcdmd 5654 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ (πΉβ€˜π‘ƒ) ∈ βˆͺ 𝐾)
2322adantr 276 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ (πΉβ€˜π‘ƒ) ∈ βˆͺ 𝐾)
247adantr 276 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))
25 simprl 529 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ 𝑧 ∈ 𝐿)
26 fvco3 5589 . . . . . . . . 9 ((𝐹:βˆͺ 𝐽⟢βˆͺ 𝐾 ∧ 𝑃 ∈ βˆͺ 𝐽) β†’ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) = (πΊβ€˜(πΉβ€˜π‘ƒ)))
2715, 21, 26syl2anc 411 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) = (πΊβ€˜(πΉβ€˜π‘ƒ)))
2827adantr 276 . . . . . . 7 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) = (πΊβ€˜(πΉβ€˜π‘ƒ)))
29 simprr 531 . . . . . . 7 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)
3028, 29eqeltrrd 2255 . . . . . 6 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ (πΊβ€˜(πΉβ€˜π‘ƒ)) ∈ 𝑧)
31 icnpimaex 13796 . . . . . 6 (((𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾) ∧ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿) ∧ (πΉβ€˜π‘ƒ) ∈ βˆͺ 𝐾) ∧ (𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)) ∧ 𝑧 ∈ 𝐿 ∧ (πΊβ€˜(πΉβ€˜π‘ƒ)) ∈ 𝑧)) β†’ βˆƒπ‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))
3218, 19, 23, 24, 25, 30, 31syl33anc 1253 . . . . 5 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ βˆƒπ‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))
3312ad2antrr 488 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ 𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽))
343ad2antrr 488 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾))
3521ad2antrr 488 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ 𝑃 ∈ βˆͺ 𝐽)
36 simplll 533 . . . . . . . 8 ((((𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ))
3736adantlll 480 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ))
38 simprl 529 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ 𝑦 ∈ 𝐾)
39 simprrl 539 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ (πΉβ€˜π‘ƒ) ∈ 𝑦)
40 icnpimaex 13796 . . . . . . 7 (((𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽) ∧ 𝐾 ∈ (TopOnβ€˜βˆͺ 𝐾) ∧ 𝑃 ∈ βˆͺ 𝐽) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘ƒ) ∈ 𝑦)) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦))
4133, 34, 35, 37, 38, 39, 40syl33anc 1253 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦))
42 imaco 5136 . . . . . . . . . . 11 ((𝐺 ∘ 𝐹) β€œ π‘₯) = (𝐺 β€œ (𝐹 β€œ π‘₯))
43 imass2 5006 . . . . . . . . . . 11 ((𝐹 β€œ π‘₯) βŠ† 𝑦 β†’ (𝐺 β€œ (𝐹 β€œ π‘₯)) βŠ† (𝐺 β€œ 𝑦))
4442, 43eqsstrid 3203 . . . . . . . . . 10 ((𝐹 β€œ π‘₯) βŠ† 𝑦 β†’ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† (𝐺 β€œ 𝑦))
45 simprrr 540 . . . . . . . . . 10 ((((𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ (𝐺 β€œ 𝑦) βŠ† 𝑧)
46 sstr2 3164 . . . . . . . . . 10 (((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† (𝐺 β€œ 𝑦) β†’ ((𝐺 β€œ 𝑦) βŠ† 𝑧 β†’ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧))
4744, 45, 46syl2imc 39 . . . . . . . . 9 ((((𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ ((𝐹 β€œ π‘₯) βŠ† 𝑦 β†’ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧))
4847adantlll 480 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ ((𝐹 β€œ π‘₯) βŠ† 𝑦 β†’ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧))
4948anim2d 337 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ ((𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦) β†’ (𝑃 ∈ π‘₯ ∧ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧)))
5049reximdv 2578 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ (βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧)))
5141, 50mpd 13 . . . . 5 (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ (𝐺 β€œ 𝑦) βŠ† 𝑧))) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧))
5232, 51rexlimddv 2599 . . . 4 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧)) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧))
5352expr 375 . . 3 ((((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) ∧ 𝑧 ∈ 𝐿) β†’ (((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧)))
5453ralrimiva 2550 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ βˆ€π‘§ ∈ 𝐿 (((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧)))
55 iscnp 13784 . . 3 ((𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽) ∧ 𝐿 ∈ (TopOnβ€˜βˆͺ 𝐿) ∧ 𝑃 ∈ βˆͺ 𝐽) β†’ ((𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)β€˜π‘ƒ) ↔ ((𝐺 ∘ 𝐹):βˆͺ 𝐽⟢βˆͺ 𝐿 ∧ βˆ€π‘§ ∈ 𝐿 (((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧)))))
5612, 6, 21, 55syl3anc 1238 . 2 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ ((𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)β€˜π‘ƒ) ↔ ((𝐺 ∘ 𝐹):βˆͺ 𝐽⟢βˆͺ 𝐿 ∧ βˆ€π‘§ ∈ 𝐿 (((𝐺 ∘ 𝐹)β€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ ((𝐺 ∘ 𝐹) β€œ π‘₯) βŠ† 𝑧)))))
5717, 54, 56mpbir2and 944 1 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ (𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)β€˜π‘ƒ))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 978   = wceq 1353   ∈ wcel 2148  βˆ€wral 2455  βˆƒwrex 2456   βŠ† wss 3131  βˆͺ cuni 3811   β€œ cima 4631   ∘ ccom 4632  βŸΆwf 5214  β€˜cfv 5218  (class class class)co 5877  Topctop 13582  TopOnctopon 13595   CnP ccnp 13771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-map 6652  df-top 13583  df-topon 13596  df-cnp 13774
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator