MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txcnp Structured version   Visualization version   GIF version
Theorem txcnp 23116
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 22746 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆπ‘Œ)
51, 2, 3, 4syl3anc 1372 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆπ‘Œ)
65fvmptelcdm 7110 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 ∈ π‘Œ)
7 txcnp.6 . . . . . 6 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜π‘))
8 txcnp.9 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡) ∈ ((𝐽 CnP 𝐿)β€˜π·))
9 cnpf2 22746 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐿 ∈ (TopOnβ€˜π‘) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐡) ∈ ((𝐽 CnP 𝐿)β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡):π‘‹βŸΆπ‘)
101, 7, 8, 9syl3anc 1372 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡):π‘‹βŸΆπ‘)
1110fvmptelcdm 7110 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐡 ∈ 𝑍)
126, 11opelxpd 5714 . . 3 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ⟨𝐴, 𝐡⟩ ∈ (π‘Œ Γ— 𝑍))
1312fmpttd 7112 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩):π‘‹βŸΆ(π‘Œ Γ— 𝑍))
14 txcnp.7 . . . . . . . . 9 (πœ‘ β†’ 𝐷 ∈ 𝑋)
15 simpr 486 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
16 opex 5464 . . . . . . . . . . . 12 ⟨𝐴, 𝐡⟩ ∈ V
17 eqid 2733 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) = (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)
1817fvmpt2 7007 . . . . . . . . . . . 12 ((π‘₯ ∈ 𝑋 ∧ ⟨𝐴, 𝐡⟩ ∈ V) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨𝐴, 𝐡⟩)
1915, 16, 18sylancl 587 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨𝐴, 𝐡⟩)
20 eqid 2733 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝑋 ↦ 𝐴) = (π‘₯ ∈ 𝑋 ↦ 𝐴)
2120fvmpt2 7007 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝑋 ∧ 𝐴 ∈ π‘Œ) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
2215, 6, 21syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
23 eqid 2733 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝑋 ↦ 𝐡) = (π‘₯ ∈ 𝑋 ↦ 𝐡)
2423fvmpt2 7007 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝑋 ∧ 𝐡 ∈ 𝑍) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯) = 𝐡)
2515, 11, 24syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯) = 𝐡)
2622, 25opeq12d 4881 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ = ⟨𝐴, 𝐡⟩)
2719, 26eqtr4d 2776 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩)
2827ralrimiva 3147 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩)
29 nffvmpt1 6900 . . . . . . . . . . 11 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·)
30 nffvmpt1 6900 . . . . . . . . . . . 12 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)
31 nffvmpt1 6900 . . . . . . . . . . . 12 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)
3230, 31nfop 4889 . . . . . . . . . . 11 β„²π‘₯⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩
3329, 32nfeq 2917 . . . . . . . . . 10 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩
34 fveq2 6889 . . . . . . . . . . 11 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·))
35 fveq2 6889 . . . . . . . . . . . 12 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·))
36 fveq2 6889 . . . . . . . . . . . 12 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·))
3735, 36opeq12d 4881 . . . . . . . . . . 11 (π‘₯ = 𝐷 β†’ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩)
3834, 37eqeq12d 2749 . . . . . . . . . 10 (π‘₯ = 𝐷 β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩))
3933, 38rspc 3601 . . . . . . . . 9 (𝐷 ∈ 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩))
4014, 28, 39sylc 65 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩)
4140eleq1d 2819 . . . . . . 7 (πœ‘ β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) ↔ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩ ∈ (𝑣 Γ— 𝑀)))
4241adantr 482 . . . . . 6 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) ↔ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩ ∈ (𝑣 Γ— 𝑀)))
433ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)β€˜π·))
44 simplrl 776 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ 𝑣 ∈ 𝐾)
45 simprl 770 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣)
46 cnpimaex 22752 . . . . . . . . . 10 (((π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)β€˜π·) ∧ 𝑣 ∈ 𝐾 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣) β†’ βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣))
4743, 44, 45, 46syl3anc 1372 . . . . . . . . 9 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣))
488ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡) ∈ ((𝐽 CnP 𝐿)β€˜π·))
49 simplrr 777 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ 𝑀 ∈ 𝐿)
50 simprr 772 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)
51 cnpimaex 22752 . . . . . . . . . 10 (((π‘₯ ∈ 𝑋 ↦ 𝐡) ∈ ((𝐽 CnP 𝐿)β€˜π·) ∧ 𝑀 ∈ 𝐿 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀) β†’ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))
5248, 49, 50, 51syl3anc 1372 . . . . . . . . 9 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))
5347, 52jca 513 . . . . . . . 8 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀)) β†’ (βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)))
5453ex 414 . . . . . . 7 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ ((((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀) β†’ (βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))))
55 opelxp 5712 . . . . . . 7 (⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩ ∈ (𝑣 Γ— 𝑀) ↔ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·) ∈ 𝑀))
56 reeanv 3227 . . . . . . 7 (βˆƒπ‘Ÿ ∈ 𝐽 βˆƒπ‘  ∈ 𝐽 ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) ↔ (βˆƒπ‘Ÿ ∈ 𝐽 (𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ βˆƒπ‘  ∈ 𝐽 (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)))
5754, 55, 563imtr4g 296 . . . . . 6 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π·)⟩ ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘Ÿ ∈ 𝐽 βˆƒπ‘  ∈ 𝐽 ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))))
5842, 57sylbid 239 . . . . 5 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘Ÿ ∈ 𝐽 βˆƒπ‘  ∈ 𝐽 ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))))
59 an4 655 . . . . . . . . . . 11 (((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) ↔ ((𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)))
60 elin 3964 . . . . . . . . . . . . . 14 (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ↔ (𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠))
6160biimpri 227 . . . . . . . . . . . . 13 ((𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠) β†’ 𝐷 ∈ (π‘Ÿ ∩ 𝑠))
6261a1i 11 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ ((𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠) β†’ 𝐷 ∈ (π‘Ÿ ∩ 𝑠)))
63 simpl 484 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) β†’ π‘Ÿ ∈ 𝐽)
64 toponss 22421 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ π‘Ÿ ∈ 𝐽) β†’ π‘Ÿ βŠ† 𝑋)
651, 63, 64syl2an 597 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ π‘Ÿ βŠ† 𝑋)
66 ssinss1 4237 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ÿ βŠ† 𝑋 β†’ (π‘Ÿ ∩ 𝑠) βŠ† 𝑋)
6766adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ (π‘Ÿ ∩ 𝑠) βŠ† 𝑋)
6867sselda 3982 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ 𝑋)
6928ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ βˆ€π‘₯ ∈ 𝑋 ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩)
70 nffvmpt1 6900 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘)
71 nffvmpt1 6900 . . . . . . . . . . . . . . . . . . . . . 22 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘)
72 nffvmpt1 6900 . . . . . . . . . . . . . . . . . . . . . 22 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)
7371, 72nfop 4889 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘₯⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩
7470, 73nfeq 2917 . . . . . . . . . . . . . . . . . . . 20 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩
75 fveq2 6889 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘))
76 fveq2 6889 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘))
77 fveq2 6889 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘))
7876, 77opeq12d 4881 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩)
7975, 78eqeq12d 2749 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑑 β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩))
8074, 79rspc 3601 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘₯) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘₯)⟩ β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩))
8168, 69, 80sylc 65 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) = ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩)
82 simpr 486 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ (π‘Ÿ ∩ 𝑠))
8382elin1d 4198 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ π‘Ÿ)
845ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆπ‘Œ)
8584ffund 6719 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ Fun (π‘₯ ∈ 𝑋 ↦ 𝐴))
8667adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘Ÿ ∩ 𝑠) βŠ† 𝑋)
8784fdmd 6726 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐴) = 𝑋)
8886, 87sseqtrrd 4023 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘Ÿ ∩ 𝑠) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐴))
8988, 82sseldd 3983 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ dom (π‘₯ ∈ 𝑋 ↦ 𝐴))
90 funfvima 7229 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (π‘₯ ∈ 𝑋 ↦ 𝐴) ∧ 𝑑 ∈ dom (π‘₯ ∈ 𝑋 ↦ 𝐴)) β†’ (𝑑 ∈ π‘Ÿ β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ)))
9185, 89, 90syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (𝑑 ∈ π‘Ÿ β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ)))
9283, 91mpd 15 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ))
9382elin2d 4199 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ 𝑠)
9410ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐡):π‘‹βŸΆπ‘)
9594ffund 6719 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ Fun (π‘₯ ∈ 𝑋 ↦ 𝐡))
9694fdmd 6726 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐡) = 𝑋)
9786, 96sseqtrrd 4023 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (π‘Ÿ ∩ 𝑠) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐡))
9897, 82sseldd 3983 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ 𝑑 ∈ dom (π‘₯ ∈ 𝑋 ↦ 𝐡))
99 funfvima 7229 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (π‘₯ ∈ 𝑋 ↦ 𝐡) ∧ 𝑑 ∈ dom (π‘₯ ∈ 𝑋 ↦ 𝐡)) β†’ (𝑑 ∈ 𝑠 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
10095, 98, 99syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ (𝑑 ∈ 𝑠 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
10193, 100mpd 15 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘) ∈ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠))
10292, 101opelxpd 5714 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ⟨((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘), ((π‘₯ ∈ 𝑋 ↦ 𝐡)β€˜π‘‘)⟩ ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
10381, 102eqeltrd 2834 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) ∧ 𝑑 ∈ (π‘Ÿ ∩ 𝑠)) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
104103ralrimiva 3147 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ βˆ€π‘‘ ∈ (π‘Ÿ ∩ 𝑠)((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
10513ffund 6719 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ Fun (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩))
106105adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ Fun (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩))
10713fdmd 6726 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ dom (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) = 𝑋)
108107adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ dom (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) = 𝑋)
10967, 108sseqtrrd 4023 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ (π‘Ÿ ∩ 𝑠) βŠ† dom (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩))
110 funimass4 6954 . . . . . . . . . . . . . . . . 17 ((Fun (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) ∧ (π‘Ÿ ∩ 𝑠) βŠ† dom (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) ↔ βˆ€π‘‘ ∈ (π‘Ÿ ∩ 𝑠)((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠))))
111106, 109, 110syl2anc 585 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) ↔ βˆ€π‘‘ ∈ (π‘Ÿ ∩ 𝑠)((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π‘‘) ∈ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠))))
112104, 111mpbird 257 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Ÿ βŠ† 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
11365, 112syldan 592 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
114113adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)))
115 xpss12 5691 . . . . . . . . . . . . 13 ((((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) βŠ† (𝑣 Γ— 𝑀))
116 sstr2 3989 . . . . . . . . . . . . 13 (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) β†’ ((((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) Γ— ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠)) βŠ† (𝑣 Γ— 𝑀) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))
117114, 115, 116syl2im 40 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ ((((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))
11862, 117anim12d 610 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (((𝐷 ∈ π‘Ÿ ∧ 𝐷 ∈ 𝑠) ∧ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀))))
11959, 118biimtrid 241 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀))))
120 topontop 22407 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
1211, 120syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐽 ∈ Top)
122 inopn 22393 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) β†’ (π‘Ÿ ∩ 𝑠) ∈ 𝐽)
1231223expb 1121 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (π‘Ÿ ∩ 𝑠) ∈ 𝐽)
124121, 123sylan 581 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (π‘Ÿ ∩ 𝑠) ∈ 𝐽)
125124adantlr 714 . . . . . . . . . 10 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (π‘Ÿ ∩ 𝑠) ∈ 𝐽)
126119, 125jctild 527 . . . . . . . . 9 (((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) ∧ (π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽)) β†’ (((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ ((π‘Ÿ ∩ 𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))))
127126expimpd 455 . . . . . . . 8 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) ∧ ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))) β†’ ((π‘Ÿ ∩ 𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))))
128 eleq2 2823 . . . . . . . . . 10 (𝑧 = (π‘Ÿ ∩ 𝑠) β†’ (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (π‘Ÿ ∩ 𝑠)))
129 imaeq2 6054 . . . . . . . . . . 11 (𝑧 = (π‘Ÿ ∩ 𝑠) β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) = ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)))
130129sseq1d 4013 . . . . . . . . . 10 (𝑧 = (π‘Ÿ ∩ 𝑠) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀) ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀)))
131128, 130anbi12d 632 . . . . . . . . 9 (𝑧 = (π‘Ÿ ∩ 𝑠) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)) ↔ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀))))
132131rspcev 3613 . . . . . . . 8 (((π‘Ÿ ∩ 𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (π‘Ÿ ∩ 𝑠) ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ (π‘Ÿ ∩ 𝑠)) βŠ† (𝑣 Γ— 𝑀))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))
133127, 132syl6 35 . . . . . . 7 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) ∧ ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
134133expd 417 . . . . . 6 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ ((π‘Ÿ ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) β†’ (((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))))
135134rexlimdvv 3211 . . . . 5 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (βˆƒπ‘Ÿ ∈ 𝐽 βˆƒπ‘  ∈ 𝐽 ((𝐷 ∈ π‘Ÿ ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ π‘Ÿ) βŠ† 𝑣) ∧ (𝐷 ∈ 𝑠 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐡) β€œ 𝑠) βŠ† 𝑀)) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
13658, 135syld 47 . . . 4 ((πœ‘ ∧ (𝑣 ∈ 𝐾 ∧ 𝑀 ∈ 𝐿)) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
137136ralrimivva 3201 . . 3 (πœ‘ β†’ βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
138 vex 3479 . . . . . 6 𝑣 ∈ V
139 vex 3479 . . . . . 6 𝑀 ∈ V
140138, 139xpex 7737 . . . . 5 (𝑣 Γ— 𝑀) ∈ V
141140rgen2w 3067 . . . 4 βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (𝑣 Γ— 𝑀) ∈ V
142 eqid 2733 . . . . 5 (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀)) = (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))
143 eleq2 2823 . . . . . 6 (𝑦 = (𝑣 Γ— 𝑀) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀)))
144 sseq2 4008 . . . . . . . 8 (𝑦 = (𝑣 Γ— 𝑀) β†’ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦 ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))
145144anbi2d 630 . . . . . . 7 (𝑦 = (𝑣 Γ— 𝑀) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦) ↔ (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
146145rexbidv 3179 . . . . . 6 (𝑦 = (𝑣 Γ— 𝑀) β†’ (βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦) ↔ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
147143, 146imbi12d 345 . . . . 5 (𝑦 = (𝑣 Γ— 𝑀) β†’ ((((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)) ↔ (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))))
148142, 147ralrnmpo 7544 . . . 4 (βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (𝑣 Γ— 𝑀) ∈ V β†’ (βˆ€π‘¦ ∈ ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))(((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)) ↔ βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀)))))
149141, 148ax-mp 5 . . 3 (βˆ€π‘¦ ∈ ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))(((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)) ↔ βˆ€π‘£ ∈ 𝐾 βˆ€π‘€ ∈ 𝐿 (((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ (𝑣 Γ— 𝑀) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† (𝑣 Γ— 𝑀))))
150137, 149sylibr 233 . 2 (πœ‘ β†’ βˆ€π‘¦ ∈ ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))(((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)))
151 topontop 22407 . . . . 5 (𝐾 ∈ (TopOnβ€˜π‘Œ) β†’ 𝐾 ∈ Top)
1522, 151syl 17 . . . 4 (πœ‘ β†’ 𝐾 ∈ Top)
153 topontop 22407 . . . . 5 (𝐿 ∈ (TopOnβ€˜π‘) β†’ 𝐿 ∈ Top)
1547, 153syl 17 . . . 4 (πœ‘ β†’ 𝐿 ∈ Top)
155 eqid 2733 . . . . 5 ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀)) = ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))
156155txval 23060 . . . 4 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) β†’ (𝐾 Γ—t 𝐿) = (topGenβ€˜ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))))
157152, 154, 156syl2anc 585 . . 3 (πœ‘ β†’ (𝐾 Γ—t 𝐿) = (topGenβ€˜ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))))
158 txtopon 23087 . . . 4 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐿 ∈ (TopOnβ€˜π‘)) β†’ (𝐾 Γ—t 𝐿) ∈ (TopOnβ€˜(π‘Œ Γ— 𝑍)))
1592, 7, 158syl2anc 585 . . 3 (πœ‘ β†’ (𝐾 Γ—t 𝐿) ∈ (TopOnβ€˜(π‘Œ Γ— 𝑍)))
1601, 157, 159, 14tgcnp 22749 . 2 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) ∈ ((𝐽 CnP (𝐾 Γ—t 𝐿))β€˜π·) ↔ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩):π‘‹βŸΆ(π‘Œ Γ— 𝑍) ∧ βˆ€π‘¦ ∈ ran (𝑣 ∈ 𝐾, 𝑀 ∈ 𝐿 ↦ (𝑣 Γ— 𝑀))(((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩)β€˜π·) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) β€œ 𝑧) βŠ† 𝑦)))))
16113, 150, 160mpbir2and 712 1 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ ⟨𝐴, 𝐡⟩) ∈ ((𝐽 CnP (𝐾 Γ—t 𝐿))β€˜π·))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   ∩ cin 3947   βŠ† wss 3948  βŸ¨cop 4634   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676  ran crn 5677   β€œ cima 5679  Fun wfun 6535  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406   ∈ cmpo 7408  topGenctg 17380  Topctop 22387  TopOnctopon 22404   CnP ccnp 22721   Γ—t ctx 23056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-map 8819  df-topgen 17386  df-top 22388  df-topon 22405  df-bases 22441  df-cnp 22724  df-tx 23058
This theorem is referenced by:  limccnp2  25401
  Copyright terms: Public domain W3C validator