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

Theorem txcnp 13642
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 13578 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷)) → (𝑥𝑋𝐴):𝑋𝑌)
51, 2, 3, 4syl3anc 1238 . . . . 5 (𝜑 → (𝑥𝑋𝐴):𝑋𝑌)
65fvmptelcdm 5668 . . . 4 ((𝜑𝑥𝑋) → 𝐴𝑌)
7 txcnp.6 . . . . . 6 (𝜑𝐿 ∈ (TopOn‘𝑍))
8 txcnp.9 . . . . . 6 (𝜑 → (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷))
9 cnpf2 13578 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷)) → (𝑥𝑋𝐵):𝑋𝑍)
101, 7, 8, 9syl3anc 1238 . . . . 5 (𝜑 → (𝑥𝑋𝐵):𝑋𝑍)
1110fvmptelcdm 5668 . . . 4 ((𝜑𝑥𝑋) → 𝐵𝑍)
126, 11opelxpd 4658 . . 3 ((𝜑𝑥𝑋) → ⟨𝐴, 𝐵⟩ ∈ (𝑌 × 𝑍))
1312fmpttd 5670 . 2 (𝜑 → (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩):𝑋⟶(𝑌 × 𝑍))
14 txcnp.7 . . . . . . . . 9 (𝜑𝐷𝑋)
15 simpr 110 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝑥𝑋)
1612elexd 2750 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ⟨𝐴, 𝐵⟩ ∈ V)
17 eqid 2177 . . . . . . . . . . . . 13 (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)
1817fvmpt2 5598 . . . . . . . . . . . 12 ((𝑥𝑋 ∧ ⟨𝐴, 𝐵⟩ ∈ V) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨𝐴, 𝐵⟩)
1915, 16, 18syl2anc 411 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨𝐴, 𝐵⟩)
20 eqid 2177 . . . . . . . . . . . . . 14 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
2120fvmpt2 5598 . . . . . . . . . . . . 13 ((𝑥𝑋𝐴𝑌) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
2215, 6, 21syl2anc 411 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
23 eqid 2177 . . . . . . . . . . . . . 14 (𝑥𝑋𝐵) = (𝑥𝑋𝐵)
2423fvmpt2 5598 . . . . . . . . . . . . 13 ((𝑥𝑋𝐵𝑍) → ((𝑥𝑋𝐵)‘𝑥) = 𝐵)
2515, 11, 24syl2anc 411 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐵)‘𝑥) = 𝐵)
2622, 25opeq12d 3786 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨𝐴, 𝐵⟩)
2719, 26eqtr4d 2213 . . . . . . . . . 10 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
2827ralrimiva 2550 . . . . . . . . 9 (𝜑 → ∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
29 nffvmpt1 5525 . . . . . . . . . . 11 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷)
30 nffvmpt1 5525 . . . . . . . . . . . 12 𝑥((𝑥𝑋𝐴)‘𝐷)
31 nffvmpt1 5525 . . . . . . . . . . . 12 𝑥((𝑥𝑋𝐵)‘𝐷)
3230, 31nfop 3794 . . . . . . . . . . 11 𝑥⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩
3329, 32nfeq 2327 . . . . . . . . . 10 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩
34 fveq2 5514 . . . . . . . . . . 11 (𝑥 = 𝐷 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷))
35 fveq2 5514 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝐷))
36 fveq2 5514 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑥𝑋𝐵)‘𝑥) = ((𝑥𝑋𝐵)‘𝐷))
3735, 36opeq12d 3786 . . . . . . . . . . 11 (𝑥 = 𝐷 → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩)
3834, 37eqeq12d 2192 . . . . . . . . . 10 (𝑥 = 𝐷 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩))
3933, 38rspc 2835 . . . . . . . . 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 13582 . . . . . . . . . 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 13582 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ 𝐷𝑋) ∧ ((𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷) ∧ 𝑤𝐿 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))
5643, 51, 45, 52, 53, 54, 55syl33anc 1253 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))
5750, 56jca 306 . . . . . . . 8 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
5857ex 115 . . . . . . 7 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → ((((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤) → (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
59 opelxp 4655 . . . . . . 7 (⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤) ↔ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤))
60 reeanv 2646 . . . . . . 7 (∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) ↔ (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
6158, 59, 603imtr4g 205 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤) → ∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
6242, 61sylbid 150 . . . . 5 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
63 an4 586 . . . . . . . . . . 11 (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) ↔ ((𝐷𝑟𝐷𝑠) ∧ (((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
64 elin 3318 . . . . . . . . . . . . . 14 (𝐷 ∈ (𝑟𝑠) ↔ (𝐷𝑟𝐷𝑠))
6564biimpri 133 . . . . . . . . . . . . 13 ((𝐷𝑟𝐷𝑠) → 𝐷 ∈ (𝑟𝑠))
6665a1i 9 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((𝐷𝑟𝐷𝑠) → 𝐷 ∈ (𝑟𝑠)))
67 simpl 109 . . . . . . . . . . . . . . . 16 ((𝑟𝐽𝑠𝐽) → 𝑟𝐽)
68 toponss 13395 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑟𝐽) → 𝑟𝑋)
691, 67, 68syl2an 289 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → 𝑟𝑋)
70 ssinss1 3364 . . . . . . . . . . . . . . . . . . . . 21 (𝑟𝑋 → (𝑟𝑠) ⊆ 𝑋)
7170adantl 277 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑟𝑋) → (𝑟𝑠) ⊆ 𝑋)
7271sselda 3155 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑋)
7328ad2antrr 488 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
74 nffvmpt1 5525 . . . . . . . . . . . . . . . . . . . . 21 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡)
75 nffvmpt1 5525 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑥𝑋𝐴)‘𝑡)
76 nffvmpt1 5525 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑥𝑋𝐵)‘𝑡)
7775, 76nfop 3794 . . . . . . . . . . . . . . . . . . . . 21 𝑥⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩
7874, 77nfeq 2327 . . . . . . . . . . . . . . . . . . . 20 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩
79 fveq2 5514 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡))
80 fveq2 5514 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝑡))
81 fveq2 5514 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → ((𝑥𝑋𝐵)‘𝑥) = ((𝑥𝑋𝐵)‘𝑡))
8280, 81opeq12d 3786 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩)
8379, 82eqeq12d 2192 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑡 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩))
8478, 83rspc 2835 . . . . . . . . . . . . . . . . . . 19 (𝑡𝑋 → (∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩))
8572, 73, 84sylc 62 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩)
86 simpr 110 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ (𝑟𝑠))
8786elin1d 3324 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑟)
885ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑥𝑋𝐴):𝑋𝑌)
8988ffund 5368 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → Fun (𝑥𝑋𝐴))
9071adantr 276 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ 𝑋)
9188fdmd 5371 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → dom (𝑥𝑋𝐴) = 𝑋)
9290, 91sseqtrrd 3194 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ dom (𝑥𝑋𝐴))
9392, 86sseldd 3156 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ dom (𝑥𝑋𝐴))
94 funfvima 5746 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝑥𝑋𝐴) ∧ 𝑡 ∈ dom (𝑥𝑋𝐴)) → (𝑡𝑟 → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟)))
9589, 93, 94syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑡𝑟 → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟)))
9687, 95mpd 13 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟))
9786elin2d 3325 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑠)
9810ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑥𝑋𝐵):𝑋𝑍)
9998ffund 5368 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → Fun (𝑥𝑋𝐵))
10098fdmd 5371 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → dom (𝑥𝑋𝐵) = 𝑋)
10190, 100sseqtrrd 3194 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ dom (𝑥𝑋𝐵))
102101, 86sseldd 3156 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ dom (𝑥𝑋𝐵))
103 funfvima 5746 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝑥𝑋𝐵) ∧ 𝑡 ∈ dom (𝑥𝑋𝐵)) → (𝑡𝑠 → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠)))
10499, 102, 103syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑡𝑠 → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠)))
10597, 104mpd 13 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠))
10696, 105opelxpd 4658 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩ ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
10785, 106eqeltrd 2254 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
108107ralrimiva 2550 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑋) → ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
10913ffund 5368 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
110109adantr 276 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑋) → Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
11113fdmd 5371 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = 𝑋)
112111adantr 276 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑋) → dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = 𝑋)
11371, 112sseqtrrd 3194 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑋) → (𝑟𝑠) ⊆ dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
114 funimass4 5565 . . . . . . . . . . . . . . . . 17 ((Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) ∧ (𝑟𝑠) ⊆ dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ↔ ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠))))
115110, 113, 114syl2anc 411 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑋) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ↔ ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠))))
116108, 115mpbird 167 . . . . . . . . . . . . . . 15 ((𝜑𝑟𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
11769, 116syldan 282 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
118117adantlr 477 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
119 xpss12 4732 . . . . . . . . . . . . 13 ((((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤) → (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ⊆ (𝑣 × 𝑤))
120 sstr2 3162 . . . . . . . . . . . . 13 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) → ((((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ⊆ (𝑣 × 𝑤) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
121118, 119, 120syl2im 38 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
12266, 121anim12d 335 . . . . . . . . . . 11 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟𝐷𝑠) ∧ (((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
12363, 122biimtrid 152 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
124 topontop 13383 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
1251, 124syl 14 . . . . . . . . . . . 12 (𝜑𝐽 ∈ Top)
126 inopn 13372 . . . . . . . . . . . . 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 4965 . . . . . . . . . . 11 (𝑧 = (𝑟𝑠) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)))
134133sseq1d 3184 . . . . . . . . . 10 (𝑧 = (𝑟𝑠) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤) ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
135132, 134anbi12d 473 . . . . . . . . 9 (𝑧 = (𝑟𝑠) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)) ↔ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
136135rspcev 2841 . . . . . . . 8 (((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))
137131, 136syl6 33 . . . . . . 7 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑟𝐽𝑠𝐽) ∧ ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
138137expd 258 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → ((𝑟𝐽𝑠𝐽) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
139138rexlimdvv 2601 . . . . 5 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
14062, 139syld 45 . . . 4 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
141140ralrimivva 2559 . . 3 (𝜑 → ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
142 vex 2740 . . . . . 6 𝑣 ∈ V
143 vex 2740 . . . . . 6 𝑤 ∈ V
144142, 143xpex 4740 . . . . 5 (𝑣 × 𝑤) ∈ V
145144rgen2w 2533 . . . 4 𝑣𝐾𝑤𝐿 (𝑣 × 𝑤) ∈ V
146 eqid 2177 . . . . 5 (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤)) = (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))
147 eleq2 2241 . . . . . 6 (𝑦 = (𝑣 × 𝑤) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤)))
148 sseq2 3179 . . . . . . . 8 (𝑦 = (𝑣 × 𝑤) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))
149148anbi2d 464 . . . . . . 7 (𝑦 = (𝑣 × 𝑤) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦) ↔ (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
150149rexbidv 2478 . . . . . 6 (𝑦 = (𝑣 × 𝑤) → (∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦) ↔ ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
151147, 150imbi12d 234 . . . . 5 (𝑦 = (𝑣 × 𝑤) → ((((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
152146, 151ralrnmpo 5986 . . . 4 (∀𝑣𝐾𝑤𝐿 (𝑣 × 𝑤) ∈ V → (∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
153145, 152ax-mp 5 . . 3 (∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
154141, 153sylibr 134 . 2 (𝜑 → ∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)))
155 topontop 13383 . . . . 5 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
1562, 155syl 14 . . . 4 (𝜑𝐾 ∈ Top)
157 topontop 13383 . . . . 5 (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top)
1587, 157syl 14 . . . 4 (𝜑𝐿 ∈ Top)
159 eqid 2177 . . . . 5 ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤)) = ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))
160159txval 13626 . . . 4 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐾 ×t 𝐿) = (topGen‘ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))))
161156, 158, 160syl2anc 411 . . 3 (𝜑 → (𝐾 ×t 𝐿) = (topGen‘ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))))
162 txtopon 13633 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑌 × 𝑍)))
1632, 7, 162syl2anc 411 . . 3 (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑌 × 𝑍)))
1641, 161, 163, 14tgcnp 13580 . 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 2737  cin 3128  wss 3129  cop 3595  cmpt 4063   × cxp 4623  dom cdm 4625  ran crn 4626  cima 4628  Fun wfun 5209  wf 5211  cfv 5215  (class class class)co 5872  cmpo 5874  topGenctg 12691  Topctop 13366  TopOnctopon 13379   CnP ccnp 13557   ×t ctx 13623
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 4117  ax-sep 4120  ax-pow 4173  ax-pr 4208  ax-un 4432  ax-setind 4535
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 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-iun 3888  df-br 4003  df-opab 4064  df-mpt 4065  df-id 4292  df-xp 4631  df-rel 4632  df-cnv 4633  df-co 4634  df-dm 4635  df-rn 4636  df-res 4637  df-ima 4638  df-iota 5177  df-fun 5217  df-fn 5218  df-f 5219  df-f1 5220  df-fo 5221  df-f1o 5222  df-fv 5223  df-ov 5875  df-oprab 5876  df-mpo 5877  df-1st 6138  df-2nd 6139  df-map 6647  df-topgen 12697  df-top 13367  df-topon 13380  df-bases 13412  df-cnp 13560  df-tx 13624
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator