Metamath Proof Explorer

Theorem txcnp

Description: If two functions are continuous at D , then the ordered pair of them is continuous at D into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses txcnp.4 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
txcnp.5 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
txcnp.6 ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
txcnp.7 ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 )
txcnp.8 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐷 ) )
txcnp.9 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( 𝐽 CnP 𝐿 ) ‘ 𝐷 ) )
Assertion txcnp ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ( 𝐽 CnP ( 𝐾 ×t 𝐿 ) ) ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 txcnp.4 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 txcnp.5 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 txcnp.6 ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
4 txcnp.7 ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 )
5 txcnp.8 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐷 ) )
6 txcnp.9 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( 𝐽 CnP 𝐿 ) ‘ 𝐷 ) )
7 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐷 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 )
8 1 2 5 7 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 )
9 8 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
10 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( 𝐽 CnP 𝐿 ) ‘ 𝐷 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ 𝑍 )
11 1 3 6 10 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ 𝑍 )
12 11 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑍 )
13 9 12 opelxpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑌 × 𝑍 ) )
14 13 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) : 𝑋 ⟶ ( 𝑌 × 𝑍 ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
16 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
17 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ )
18 17 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ V ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ⟨ 𝐴 , 𝐵 ⟩ )
19 15 16 18 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ⟨ 𝐴 , 𝐵 ⟩ )
20 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
21 20 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
22 15 9 21 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
23 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
24 23 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐵 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
25 15 12 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
26 22 25 opeq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
27 19 26 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ )
28 27 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ )
29 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 )
30 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 )
31 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 )
32 30 31 nfop ⊢ Ⅎ 𝑥 ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩
33 29 32 nfeq ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩
34 fveq2 ⊢ ( 𝑥 = 𝐷 → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) )
35 fveq2 ⊢ ( 𝑥 = 𝐷 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) )
36 fveq2 ⊢ ( 𝑥 = 𝐷 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) )
37 35 36 opeq12d ⊢ ( 𝑥 = 𝐷 → ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩ )
38 34 37 eqeq12d ⊢ ( 𝑥 = 𝐷 → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ↔ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩ ) )
39 33 38 rspc ⊢ ( 𝐷 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩ ) )
40 4 28 39 sylc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩ )
41 40 eleq1d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ ( 𝑣 × 𝑤 ) ↔ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩ ∈ ( 𝑣 × 𝑤 ) ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ ( 𝑣 × 𝑤 ) ↔ ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩ ∈ ( 𝑣 × 𝑤 ) ) )
43 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐷 ) )
44 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) ) → 𝑣 ∈ 𝐾 )
45 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 )
46 cnpimaex ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐷 ) ∧ 𝑣 ∈ 𝐾 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ) → ∃ 𝑟 ∈ 𝐽 ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) )
47 43 44 45 46 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) ) → ∃ 𝑟 ∈ 𝐽 ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) )
48 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( 𝐽 CnP 𝐿 ) ‘ 𝐷 ) )
49 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) ) → 𝑤 ∈ 𝐿 )
50 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 )
51 cnpimaex ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( 𝐽 CnP 𝐿 ) ‘ 𝐷 ) ∧ 𝑤 ∈ 𝐿 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) → ∃ 𝑠 ∈ 𝐽 ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) )
52 48 49 50 51 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) ) → ∃ 𝑠 ∈ 𝐽 ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) )
53 47 52 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) ) → ( ∃ 𝑟 ∈ 𝐽 ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ∃ 𝑠 ∈ 𝐽 ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) )
54 53 ex ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) → ( ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) → ( ∃ 𝑟 ∈ 𝐽 ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ∃ 𝑠 ∈ 𝐽 ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) ) )
55 opelxp ⊢ ( ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩ ∈ ( 𝑣 × 𝑤 ) ↔ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ∈ 𝑤 ) )
56 reeanv ⊢ ( ∃ 𝑟 ∈ 𝐽 ∃ 𝑠 ∈ 𝐽 ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) ↔ ( ∃ 𝑟 ∈ 𝐽 ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ∃ 𝑠 ∈ 𝐽 ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) )
57 54 55 56 3imtr4g ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) → ( ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝐷 ) ⟩ ∈ ( 𝑣 × 𝑤 ) → ∃ 𝑟 ∈ 𝐽 ∃ 𝑠 ∈ 𝐽 ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) ) )
58 42 57 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ ( 𝑣 × 𝑤 ) → ∃ 𝑟 ∈ 𝐽 ∃ 𝑠 ∈ 𝐽 ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) ) )
59 an4 ⊢ ( ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) ↔ ( ( 𝐷 ∈ 𝑟 ∧ 𝐷 ∈ 𝑠 ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) )
60 elin ⊢ ( 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) ↔ ( 𝐷 ∈ 𝑟 ∧ 𝐷 ∈ 𝑠 ) )
61 60 biimpri ⊢ ( ( 𝐷 ∈ 𝑟 ∧ 𝐷 ∈ 𝑠 ) → 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) )
62 61 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( ( 𝐷 ∈ 𝑟 ∧ 𝐷 ∈ 𝑠 ) → 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) ) )
63 simpl ⊢ ( ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) → 𝑟 ∈ 𝐽 )
64 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑟 ∈ 𝐽 ) → 𝑟 ⊆ 𝑋 )
65 1 63 64 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → 𝑟 ⊆ 𝑋 )
66 ssinss1 ⊢ ( 𝑟 ⊆ 𝑋 → ( 𝑟 ∩ 𝑠 ) ⊆ 𝑋 )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) → ( 𝑟 ∩ 𝑠 ) ⊆ 𝑋 )
68 67 sselda ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → 𝑡 ∈ 𝑋 )
69 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ )
70 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 )
71 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 )
72 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 )
73 71 72 nfop ⊢ Ⅎ 𝑥 ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ⟩
74 70 73 nfeq ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ⟩
75 fveq2 ⊢ ( 𝑥 = 𝑡 → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 ) )
76 fveq2 ⊢ ( 𝑥 = 𝑡 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) )
77 fveq2 ⊢ ( 𝑥 = 𝑡 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) )
78 76 77 opeq12d ⊢ ( 𝑥 = 𝑡 → ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ⟩ )
79 75 78 eqeq12d ⊢ ( 𝑥 = 𝑡 → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ↔ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ⟩ ) )
80 74 79 rspc ⊢ ( 𝑡 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑥 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ⟩ ) )
81 68 69 80 sylc ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 ) = ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ⟩ )
82 simpr ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) )
83 82 elin1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → 𝑡 ∈ 𝑟 )
84 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑌 )
85 84 ffund ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → Fun ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
86 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( 𝑟 ∩ 𝑠 ) ⊆ 𝑋 )
87 84 fdmd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → dom ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = 𝑋 )
88 86 87 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( 𝑟 ∩ 𝑠 ) ⊆ dom ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
89 88 82 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → 𝑡 ∈ dom ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
90 funfvima ⊢ ( ( Fun ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∧ 𝑡 ∈ dom ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) → ( 𝑡 ∈ 𝑟 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) ∈ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ) )
91 85 89 90 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( 𝑡 ∈ 𝑟 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) ∈ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ) )
92 83 91 mpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) ∈ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) )
93 82 elin2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → 𝑡 ∈ 𝑠 )
94 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ 𝑍 )
95 94 ffund ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → Fun ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
96 94 fdmd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
97 86 96 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( 𝑟 ∩ 𝑠 ) ⊆ dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
98 97 82 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → 𝑡 ∈ dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
99 funfvima ⊢ ( ( Fun ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∧ 𝑡 ∈ dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) → ( 𝑡 ∈ 𝑠 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ∈ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) )
100 95 98 99 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( 𝑡 ∈ 𝑠 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ∈ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) )
101 93 100 mpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ∈ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) )
102 92 101 opelxpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ⟨ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) , ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑡 ) ⟩ ∈ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) )
103 81 102 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) ∧ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 ) ∈ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) )
104 103 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) → ∀ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 ) ∈ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) )
105 14 ffund ⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
106 105 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) → Fun ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
107 14 fdmd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑋 )
108 107 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) → dom ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑋 )
109 67 108 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) → ( 𝑟 ∩ 𝑠 ) ⊆ dom ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
110 funimass4 ⊢ ( ( Fun ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝑟 ∩ 𝑠 ) ⊆ dom ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) ↔ ∀ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 ) ∈ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) ) )
111 106 109 110 syl2anc ⊢ ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) ↔ ∀ 𝑡 ∈ ( 𝑟 ∩ 𝑠 ) ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑡 ) ∈ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) ) )
112 104 111 mpbird ⊢ ( ( 𝜑 ∧ 𝑟 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) )
113 65 112 syldan ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) )
114 113 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) )
115 xpss12 ⊢ ( ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) )
116 sstr2 ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) → ( ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) × ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) )
117 114 115 116 syl2im ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) )
118 62 117 anim12d ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( ( ( 𝐷 ∈ 𝑟 ∧ 𝐷 ∈ 𝑠 ) ∧ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) → ( 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
119 59 118 biimtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) → ( 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
120 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
121 1 120 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
122 inopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) → ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 )
123 122 3expb ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 )
124 121 123 sylan ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 )
125 124 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 )
126 119 125 jctild ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) ∧ ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ) → ( ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) → ( ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ∧ ( 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) ) ) )
127 126 expimpd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) → ( ( ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ∧ ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) ) → ( ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ∧ ( 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) ) ) )
128 eleq2 ⊢ ( 𝑧 = ( 𝑟 ∩ 𝑠 ) → ( 𝐷 ∈ 𝑧 ↔ 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) ) )
129 imaeq2 ⊢ ( 𝑧 = ( 𝑟 ∩ 𝑠 ) → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) )
130 129 sseq1d ⊢ ( 𝑧 = ( 𝑟 ∩ 𝑠 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) )
131 128 130 anbi12d ⊢ ( 𝑧 = ( 𝑟 ∩ 𝑠 ) → ( ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ↔ ( 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
132 131 rspcev ⊢ ( ( ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ∧ ( 𝐷 ∈ ( 𝑟 ∩ 𝑠 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟 ∩ 𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) )
133 127 132 syl6 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) → ( ( ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) ∧ ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
134 133 expd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) → ( ( 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) → ( ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) ) )
135 134 rexlimdvv ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) → ( ∃ 𝑟 ∈ 𝐽 ∃ 𝑠 ∈ 𝐽 ( ( 𝐷 ∈ 𝑟 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷 ∈ 𝑠 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
136 58 135 syld ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐾 ∧ 𝑤 ∈ 𝐿 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ ( 𝑣 × 𝑤 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
137 136 ralrimivva ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐾 ∀ 𝑤 ∈ 𝐿 ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ ( 𝑣 × 𝑤 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
138 vex ⊢ 𝑣 ∈ V
139 vex ⊢ 𝑤 ∈ V
140 138 139 xpex ⊢ ( 𝑣 × 𝑤 ) ∈ V
141 140 rgen2w ⊢ ∀ 𝑣 ∈ 𝐾 ∀ 𝑤 ∈ 𝐿 ( 𝑣 × 𝑤 ) ∈ V
142 eqid ⊢ ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) ) = ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) )
143 eleq2 ⊢ ( 𝑦 = ( 𝑣 × 𝑤 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ 𝑦 ↔ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ ( 𝑣 × 𝑤 ) ) )
144 sseq2 ⊢ ( 𝑦 = ( 𝑣 × 𝑤 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ 𝑦 ↔ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) )
145 144 anbi2d ⊢ ( 𝑦 = ( 𝑣 × 𝑤 ) → ( ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ 𝑦 ) ↔ ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
146 145 rexbidv ⊢ ( 𝑦 = ( 𝑣 × 𝑤 ) → ( ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ 𝑦 ) ↔ ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
147 143 146 imbi12d ⊢ ( 𝑦 = ( 𝑣 × 𝑤 ) → ( ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ 𝑦 ) ) ↔ ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ ( 𝑣 × 𝑤 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) ) )
148 142 147 ralrnmpo ⊢ ( ∀ 𝑣 ∈ 𝐾 ∀ 𝑤 ∈ 𝐿 ( 𝑣 × 𝑤 ) ∈ V → ( ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) ) ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ 𝑦 ) ) ↔ ∀ 𝑣 ∈ 𝐾 ∀ 𝑤 ∈ 𝐿 ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ ( 𝑣 × 𝑤 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) ) )
149 141 148 ax-mp ⊢ ( ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) ) ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ 𝑦 ) ) ↔ ∀ 𝑣 ∈ 𝐾 ∀ 𝑤 ∈ 𝐿 ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ ( 𝑣 × 𝑤 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
150 137 149 sylibr ⊢ ( 𝜑 → ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) ) ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ 𝑦 ) ) )
151 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
152 2 151 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
153 topontop ⊢ ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) → 𝐿 ∈ Top )
154 3 153 syl ⊢ ( 𝜑 → 𝐿 ∈ Top )
155 eqid ⊢ ran ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) ) = ran ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) )
156 155 txval ⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ) → ( 𝐾 ×t 𝐿 ) = ( topGen ‘ ran ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) ) ) )
157 152 154 156 syl2anc ⊢ ( 𝜑 → ( 𝐾 ×t 𝐿 ) = ( topGen ‘ ran ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) ) ) )
158 txtopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑌 × 𝑍 ) ) )
159 2 3 158 syl2anc ⊢ ( 𝜑 → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑌 × 𝑍 ) ) )
160 1 157 159 4 tgcnp ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ( 𝐽 CnP ( 𝐾 ×t 𝐿 ) ) ‘ 𝐷 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) : 𝑋 ⟶ ( 𝑌 × 𝑍 ) ∧ ∀ 𝑦 ∈ ran ( 𝑣 ∈ 𝐾 , 𝑤 ∈ 𝐿 ↦ ( 𝑣 × 𝑤 ) ) ( ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝐷 ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
161 14 150 160 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ( 𝐽 CnP ( 𝐾 ×t 𝐿 ) ) ‘ 𝐷 ) )