ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  txcnp GIF version

Theorem txcnp 13810
Description: If two functions are continuous at 𝐷, then the ordered pair of them is continuous at 𝐷 into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
txcnp.4 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
txcnp.5 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
txcnp.6 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜π‘))
txcnp.7 (πœ‘ β†’ 𝐷 ∈ 𝑋)
txcnp.8 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)β€˜π·))
txcnp.9 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡) ∈ ((𝐽 CnP 𝐿)β€˜π·))
Assertion
Ref Expression
txcnp (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) ∈ ((𝐽 CnP (𝐾 Γ—t 𝐿))β€˜π·))
Distinct variable groups:   πœ‘,π‘₯   π‘₯,π‘Œ   π‘₯,𝑍   π‘₯,𝐷   π‘₯,𝑋
Allowed substitution hints:   𝐴(π‘₯)   𝐡(π‘₯)   𝐽(π‘₯)   𝐾(π‘₯)   𝐿(π‘₯)

Proof of Theorem txcnp
Dummy variables 𝑠 π‘Ÿ 𝑑 𝑣 𝑀 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 txcnp.4 . . . . . 6 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
2 txcnp.5 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
3 txcnp.8 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)β€˜π·))
4 cnpf2 13746 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆπ‘Œ)
51, 2, 3, 4syl3anc 1238 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆπ‘Œ)
65fvmptelcdm 5671 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 ∈ π‘Œ)
7 txcnp.6 . . . . . 6 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜π‘))
8 txcnp.9 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡) ∈ ((𝐽 CnP 𝐿)β€˜π·))
9 cnpf2 13746 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐿 ∈ (TopOnβ€˜π‘) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐡) ∈ ((𝐽 CnP 𝐿)β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡):π‘‹βŸΆπ‘)
101, 7, 8, 9syl3anc 1238 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡):π‘‹βŸΆπ‘)
1110fvmptelcdm 5671 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐡 ∈ 𝑍)
126, 11opelxpd 4661 . . 3 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ⟨𝐴, 𝐡⟩ ∈ (π‘Œ Γ— 𝑍))
1312fmpttd 5673 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩):π‘‹βŸΆ(π‘Œ Γ— 𝑍))
14 txcnp.7 . . . . . . . . 9 (πœ‘ β†’ 𝐷 ∈ 𝑋)
15 simpr 110 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
1612elexd 2752 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ⟨𝐴, 𝐡⟩ ∈ V)
17 eqid 2177 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) = (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)
1817fvmpt2 5601 . . . . . . . . . . . 12 ((π‘₯ ∈ 𝑋 ∧ ⟨𝐴, 𝐡⟩ ∈ V) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨𝐴, 𝐡⟩)
1915, 16, 18syl2anc 411 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨𝐴, 𝐡⟩)
20 eqid 2177 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝑋 ↦ 𝐴) = (π‘₯ ∈ 𝑋 ↦ 𝐴)
2120fvmpt2 5601 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝑋 ∧ 𝐴 ∈ π‘Œ) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
2215, 6, 21syl2anc 411 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
23 eqid 2177 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝑋 ↦ 𝐡) = (π‘₯ ∈ 𝑋 ↦ 𝐡)
2423fvmpt2 5601 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝑋 ∧ 𝐡 ∈ 𝑍) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯) = 𝐡)
2515, 11, 24syl2anc 411 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯) = 𝐡)
2622, 25opeq12d 3788 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ = ⟨𝐴, 𝐡⟩)
2719, 26eqtr4d 2213 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩)
2827ralrimiva 2550 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩)
29 nffvmpt1 5528 . . . . . . . . . . 11 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·)
30 nffvmpt1 5528 . . . . . . . . . . . 12 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)
31 nffvmpt1 5528 . . . . . . . . . . . 12 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)
3230, 31nfop 3796 . . . . . . . . . . 11 β„²π‘₯⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩
3329, 32nfeq 2327 . . . . . . . . . 10 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩
34 fveq2 5517 . . . . . . . . . . 11 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·))
35 fveq2 5517 . . . . . . . . . . . 12 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·))
36 fveq2 5517 . . . . . . . . . . . 12 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·))
3735, 36opeq12d 3788 . . . . . . . . . . 11 (π‘₯ = 𝐷 β†’ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩)
3834, 37eqeq12d 2192 . . . . . . . . . 10 (π‘₯ = 𝐷 β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩))
3933, 38rspc 2837 . . . . . . . . 9 (𝐷 ∈ 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩))
4014, 28, 39sylc 62 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩)
4140eleq1d 2246 . . . . . . 7 (πœ‘ β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) ↔ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩ ∈ (𝑣 Γ— 𝑀)))
4241adantr 276 . . . . . 6 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) ↔ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩ ∈ (𝑣 Γ— 𝑀)))
431ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
442ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
4514ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ 𝐷 ∈ 𝑋)
463ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)β€˜π·))
47 simplrl 535 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ 𝑣 ∈ 𝐾)
48 simprl 529 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣)
49 icnpimaex 13750 . . . . . . . . . 10 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐷 ∈ 𝑋) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)β€˜π·) ∧ 𝑣 ∈ 𝐾 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣)) β†’ βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣))
5043, 44, 45, 46, 47, 48, 49syl33anc 1253 . . . . . . . . 9 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣))
517ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ 𝐿 ∈ (TopOnβ€˜π‘))
528ad2antrr 488 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡) ∈ ((𝐽 CnP 𝐿)β€˜π·))
53 simplrr 536 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ 𝑀 ∈ 𝐿)
54 simprr 531 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)
55 icnpimaex 13750 . . . . . . . . . 10 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐿 ∈ (TopOnβ€˜π‘) ∧ 𝐷 ∈ 𝑋) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) ∈ ((𝐽 CnP 𝐿)β€˜π·) ∧ 𝑀 ∈ 𝐿 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))
5643, 51, 45, 52, 53, 54, 55syl33anc 1253 . . . . . . . . 9 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))
5750, 56jca 306 . . . . . . . 8 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ (βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)))
5857ex 115 . . . . . . 7 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ ((((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀) β†’ (βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))))
59 opelxp 4658 . . . . . . 7 (⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩ ∈ (𝑣 Γ— 𝑀) ↔ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀))
60 reeanv 2647 . . . . . . 7 (βˆƒπ‘Ÿ ∈ 𝐽 βˆƒπ‘  ∈ 𝐽 ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) ↔ (βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)))
6158, 59, 603imtr4g 205 . . . . . 6 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩ ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘Ÿ ∈ 𝐽 βˆƒπ‘  ∈ 𝐽 ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))))
6242, 61sylbid 150 . . . . 5 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘Ÿ ∈ 𝐽 βˆƒπ‘  ∈ 𝐽 ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))))
63 an4 586 . . . . . . . . . . 11 (((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) ↔ ((𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)))
64 elin 3320 . . . . . . . . . . . . . 14 (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ↔ (𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠))
6564biimpri 133 . . . . . . . . . . . . 13 ((𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠) β†’ 𝐷 ∈ (π‘Ÿ ∩ 𝑠))
6665a1i 9 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ ((𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠) β†’ 𝐷 ∈ (π‘Ÿ ∩ 𝑠)))
67 simpl 109 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) β†’ π‘Ÿ ∈ 𝐽)
68 toponss 13565 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ π‘Ÿ ∈ 𝐽) β†’ π‘Ÿ βŠ† 𝑋)
691, 67, 68syl2an 289 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ π‘Ÿ βŠ† 𝑋)
70 ssinss1 3366 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ÿ βŠ† 𝑋 β†’ (π‘Ÿ ∩ 𝑠) βŠ† 𝑋)
7170adantl 277 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ (π‘Ÿ ∩ 𝑠) βŠ† 𝑋)
7271sselda 3157 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ 𝑋)
7328ad2antrr 488 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ βˆ€π‘₯ ∈ 𝑋 ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩)
74 nffvmpt1 5528 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘)
75 nffvmpt1 5528 . . . . . . . . . . . . . . . . . . . . . 22 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘)
76 nffvmpt1 5528 . . . . . . . . . . . . . . . . . . . . . 22 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)
7775, 76nfop 3796 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘₯⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩
7874, 77nfeq 2327 . . . . . . . . . . . . . . . . . . . 20 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩
79 fveq2 5517 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘))
80 fveq2 5517 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘))
81 fveq2 5517 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘))
8280, 81opeq12d 3788 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩)
8379, 82eqeq12d 2192 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑑 β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩))
8478, 83rspc 2837 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩))
8572, 73, 84sylc 62 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩)
86 simpr 110 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ (π‘Ÿ ∩ 𝑠))
8786elin1d 3326 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ π‘Ÿ)
885ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆπ‘Œ)
8988ffund 5371 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ Fun (π‘₯ ∈ 𝑋 ↦ 𝐴))
9071adantr 276 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘Ÿ ∩ 𝑠) βŠ† 𝑋)
9188fdmd 5374 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐴) = 𝑋)
9290, 91sseqtrrd 3196 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘Ÿ ∩ 𝑠) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐴))
9392, 86sseldd 3158 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ dom (π‘₯ ∈ 𝑋 ↦ 𝐴))
94 funfvima 5750 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (π‘₯ ∈ 𝑋 ↦ 𝐴) ∧ 𝑑 ∈ dom (π‘₯ ∈ 𝑋 ↦ 𝐴)) β†’ (𝑑 ∈ π‘Ÿ β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ)))
9589, 93, 94syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (𝑑 ∈ π‘Ÿ β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ)))
9687, 95mpd 13 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ))
9786elin2d 3327 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ 𝑠)
9810ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡):π‘‹βŸΆπ‘)
9998ffund 5371 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ Fun (π‘₯ ∈ 𝑋 ↦ 𝐡))
10098fdmd 5374 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐡) = 𝑋)
10190, 100sseqtrrd 3196 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘Ÿ ∩ 𝑠) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐡))
102101, 86sseldd 3158 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ dom (π‘₯ ∈ 𝑋 ↦ 𝐡))
103 funfvima 5750 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (π‘₯ ∈ 𝑋 ↦ 𝐡) ∧ 𝑑 ∈ dom (π‘₯ ∈ 𝑋 ↦ 𝐡)) β†’ (𝑑 ∈ 𝑠 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
10499, 102, 103syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (𝑑 ∈ 𝑠 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
10597, 104mpd 13 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠))
10696, 105opelxpd 4661 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩ ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
10785, 106eqeltrd 2254 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
108107ralrimiva 2550 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ βˆ€π‘‘ ∈ (π‘Ÿ ∩ 𝑠)((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
10913ffund 5371 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ Fun (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩))
110109adantr 276 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ Fun (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩))
11113fdmd 5374 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ dom (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) = 𝑋)
112111adantr 276 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ dom (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) = 𝑋)
11371, 112sseqtrrd 3196 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ (π‘Ÿ ∩ 𝑠) βŠ† dom (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩))
114 funimass4 5568 . . . . . . . . . . . . . . . . 17 ((Fun (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) ∧ (π‘Ÿ ∩ 𝑠) βŠ† dom (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) ↔ βˆ€π‘‘ ∈ (π‘Ÿ ∩ 𝑠)((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠))))
115110, 113, 114syl2anc 411 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) ↔ βˆ€π‘‘ ∈ (π‘Ÿ ∩ 𝑠)((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠))))
116108, 115mpbird 167 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
11769, 116syldan 282 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
118117adantlr 477 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
119 xpss12 4735 . . . . . . . . . . . . 13 ((((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) βŠ† (𝑣 Γ— 𝑀))
120 sstr2 3164 . . . . . . . . . . . . 13 (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) β†’ ((((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) βŠ† (𝑣 Γ— 𝑀) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))
121118, 119, 120syl2im 38 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ ((((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))
12266, 121anim12d 335 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (((𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀))))
12363, 122biimtrid 152 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀))))
124 topontop 13553 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
1251, 124syl 14 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐽 ∈ Top)
126 inopn 13542 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) β†’ (π‘Ÿ ∩ 𝑠) ∈ 𝐽)
1271263expb 1204 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (π‘Ÿ ∩ 𝑠) ∈ 𝐽)
128125, 127sylan 283 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (π‘Ÿ ∩ 𝑠) ∈ 𝐽)
129128adantlr 477 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (π‘Ÿ ∩ 𝑠) ∈ 𝐽)
130123, 129jctild 316 . . . . . . . . 9 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ ((π‘Ÿ ∩ 𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))))
131130expimpd 363 . . . . . . . 8 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) ∧ ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))) β†’ ((π‘Ÿ ∩ 𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))))
132 eleq2 2241 . . . . . . . . . 10 (𝑧 = (π‘Ÿ ∩ 𝑠) β†’ (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (π‘Ÿ ∩ 𝑠)))
133 imaeq2 4968 . . . . . . . . . . 11 (𝑧 = (π‘Ÿ ∩ 𝑠) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) = ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)))
134133sseq1d 3186 . . . . . . . . . 10 (𝑧 = (π‘Ÿ ∩ 𝑠) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀) ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))
135132, 134anbi12d 473 . . . . . . . . 9 (𝑧 = (π‘Ÿ ∩ 𝑠) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)) ↔ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀))))
136135rspcev 2843 . . . . . . . 8 (((π‘Ÿ ∩ 𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))
137131, 136syl6 33 . . . . . . 7 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) ∧ ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
138137expd 258 . . . . . 6 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ ((π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) β†’ (((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))))
139138rexlimdvv 2601 . . . . 5 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (βˆƒπ‘Ÿ ∈ 𝐽 βˆƒπ‘  ∈ 𝐽 ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
14062, 139syld 45 . . . 4 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
141140ralrimivva 2559 . . 3 (πœ‘ β†’ βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
142 vex 2742 . . . . . 6 𝑣 ∈ V
143 vex 2742 . . . . . 6 𝑀 ∈ V
144142, 143xpex 4743 . . . . 5 (𝑣 Γ— 𝑀) ∈ V
145144rgen2w 2533 . . . 4 βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (𝑣 Γ— 𝑀) ∈ V
146 eqid 2177 . . . . 5 (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀)) = (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))
147 eleq2 2241 . . . . . 6 (𝑦 = (𝑣 Γ— 𝑀) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀)))
148 sseq2 3181 . . . . . . . 8 (𝑦 = (𝑣 Γ— 𝑀) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦 ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))
149148anbi2d 464 . . . . . . 7 (𝑦 = (𝑣 Γ— 𝑀) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦) ↔ (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
150149rexbidv 2478 . . . . . 6 (𝑦 = (𝑣 Γ— 𝑀) β†’ (βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦) ↔ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
151147, 150imbi12d 234 . . . . 5 (𝑦 = (𝑣 Γ— 𝑀) β†’ ((((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)) ↔ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))))
152146, 151ralrnmpo 5991 . . . 4 (βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (𝑣 Γ— 𝑀) ∈ V β†’ (βˆ€π‘¦ ∈ ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))(((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)) ↔ βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))))
153145, 152ax-mp 5 . . 3 (βˆ€π‘¦ ∈ ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))(((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)) ↔ βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
154141, 153sylibr 134 . 2 (πœ‘ β†’ βˆ€π‘¦ ∈ ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))(((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)))
155 topontop 13553 . . . . 5 (𝐾 ∈ (TopOnβ€˜π‘Œ) β†’ 𝐾 ∈ Top)
1562, 155syl 14 . . . 4 (πœ‘ β†’ 𝐾 ∈ Top)
157 topontop 13553 . . . . 5 (𝐿 ∈ (TopOnβ€˜π‘) β†’ 𝐿 ∈ Top)
1587, 157syl 14 . . . 4 (πœ‘ β†’ 𝐿 ∈ Top)
159 eqid 2177 . . . . 5 ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀)) = ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))
160159txval 13794 . . . 4 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) β†’ (𝐾 Γ—t 𝐿) = (topGenβ€˜ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))))
161156, 158, 160syl2anc 411 . . 3 (πœ‘ β†’ (𝐾 Γ—t 𝐿) = (topGenβ€˜ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))))
162 txtopon 13801 . . . 4 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐿 ∈ (TopOnβ€˜π‘)) β†’ (𝐾 Γ—t 𝐿) ∈ (TopOnβ€˜(π‘Œ Γ— 𝑍)))
1632, 7, 162syl2anc 411 . . 3 (πœ‘ β†’ (𝐾 Γ—t 𝐿) ∈ (TopOnβ€˜(π‘Œ Γ— 𝑍)))
1641, 161, 163, 14tgcnp 13748 . 2 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) ∈ ((𝐽 CnP (𝐾 Γ—t 𝐿))β€˜π·) ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩):π‘‹βŸΆ(π‘Œ Γ— 𝑍) ∧ βˆ€π‘¦ ∈ ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))(((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)))))
16513, 154, 164mpbir2and 944 1 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) ∈ ((𝐽 CnP (𝐾 Γ—t 𝐿))β€˜π·))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  βˆ€wral 2455  βˆƒwrex 2456  Vcvv 2739   ∩ cin 3130   βŠ† wss 3131  βŸ¨cop 3597   ↦ cmpt 4066   Γ— cxp 4626  dom cdm 4628  ran crn 4629   β€œ cima 4631  Fun wfun 5212  βŸΆwf 5214  β€˜cfv 5218  (class class class)co 5877   ∈ cmpo 5879  topGenctg 12708  Topctop 13536  TopOnctopon 13549   CnP ccnp 13725   Γ—t ctx 13791
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-nul 3425  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-topgen 12714  df-top 13537  df-topon 13550  df-bases 13582  df-cnp 13728  df-tx 13792
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator