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 fvmptelrn ( ( 𝜑𝑥𝑋 ) → 𝐴𝑌 )
10 cnpf2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ ( 𝑥𝑋𝐵 ) ∈ ( ( 𝐽 CnP 𝐿 ) ‘ 𝐷 ) ) → ( 𝑥𝑋𝐵 ) : 𝑋𝑍 )
11 1 3 6 10 syl3anc ( 𝜑 → ( 𝑥𝑋𝐵 ) : 𝑋𝑍 )
12 11 fvmptelrn ( ( 𝜑𝑥𝑋 ) → 𝐵𝑍 )
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 syl5bi ( ( ( 𝜑 ∧ ( 𝑣𝐾𝑤𝐿 ) ) ∧ ( 𝑟𝐽𝑠𝐽 ) ) → ( ( ( 𝐷𝑟 ∧ ( ( 𝑥𝑋𝐴 ) “ 𝑟 ) ⊆ 𝑣 ) ∧ ( 𝐷𝑠 ∧ ( ( 𝑥𝑋𝐵 ) “ 𝑠 ) ⊆ 𝑤 ) ) → ( 𝐷 ∈ ( 𝑟𝑠 ) ∧ ( ( 𝑥𝑋 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) “ ( 𝑟𝑠 ) ) ⊆ ( 𝑣 × 𝑤 ) ) ) )
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 𝐿 ) ) ‘ 𝐷 ) )