MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txcnp Structured version   Visualization version   GIF version

Theorem txcnp 23628
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 23258 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷)) → (𝑥𝑋𝐴):𝑋𝑌)
51, 2, 3, 4syl3anc 1373 . . . . 5 (𝜑 → (𝑥𝑋𝐴):𝑋𝑌)
65fvmptelcdm 7133 . . . 4 ((𝜑𝑥𝑋) → 𝐴𝑌)
7 txcnp.6 . . . . . 6 (𝜑𝐿 ∈ (TopOn‘𝑍))
8 txcnp.9 . . . . . 6 (𝜑 → (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷))
9 cnpf2 23258 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷)) → (𝑥𝑋𝐵):𝑋𝑍)
101, 7, 8, 9syl3anc 1373 . . . . 5 (𝜑 → (𝑥𝑋𝐵):𝑋𝑍)
1110fvmptelcdm 7133 . . . 4 ((𝜑𝑥𝑋) → 𝐵𝑍)
126, 11opelxpd 5724 . . 3 ((𝜑𝑥𝑋) → ⟨𝐴, 𝐵⟩ ∈ (𝑌 × 𝑍))
1312fmpttd 7135 . 2 (𝜑 → (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩):𝑋⟶(𝑌 × 𝑍))
14 txcnp.7 . . . . . . . . 9 (𝜑𝐷𝑋)
15 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝑥𝑋)
16 opex 5469 . . . . . . . . . . . 12 𝐴, 𝐵⟩ ∈ V
17 eqid 2737 . . . . . . . . . . . . 13 (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)
1817fvmpt2 7027 . . . . . . . . . . . 12 ((𝑥𝑋 ∧ ⟨𝐴, 𝐵⟩ ∈ V) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨𝐴, 𝐵⟩)
1915, 16, 18sylancl 586 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨𝐴, 𝐵⟩)
20 eqid 2737 . . . . . . . . . . . . . 14 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
2120fvmpt2 7027 . . . . . . . . . . . . 13 ((𝑥𝑋𝐴𝑌) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
2215, 6, 21syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
23 eqid 2737 . . . . . . . . . . . . . 14 (𝑥𝑋𝐵) = (𝑥𝑋𝐵)
2423fvmpt2 7027 . . . . . . . . . . . . 13 ((𝑥𝑋𝐵𝑍) → ((𝑥𝑋𝐵)‘𝑥) = 𝐵)
2515, 11, 24syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐵)‘𝑥) = 𝐵)
2622, 25opeq12d 4881 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨𝐴, 𝐵⟩)
2719, 26eqtr4d 2780 . . . . . . . . . 10 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
2827ralrimiva 3146 . . . . . . . . 9 (𝜑 → ∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
29 nffvmpt1 6917 . . . . . . . . . . 11 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷)
30 nffvmpt1 6917 . . . . . . . . . . . 12 𝑥((𝑥𝑋𝐴)‘𝐷)
31 nffvmpt1 6917 . . . . . . . . . . . 12 𝑥((𝑥𝑋𝐵)‘𝐷)
3230, 31nfop 4889 . . . . . . . . . . 11 𝑥⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩
3329, 32nfeq 2919 . . . . . . . . . 10 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩
34 fveq2 6906 . . . . . . . . . . 11 (𝑥 = 𝐷 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷))
35 fveq2 6906 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝐷))
36 fveq2 6906 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑥𝑋𝐵)‘𝑥) = ((𝑥𝑋𝐵)‘𝐷))
3735, 36opeq12d 4881 . . . . . . . . . . 11 (𝑥 = 𝐷 → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩)
3834, 37eqeq12d 2753 . . . . . . . . . 10 (𝑥 = 𝐷 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩))
3933, 38rspc 3610 . . . . . . . . 9 (𝐷𝑋 → (∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩))
4014, 28, 39sylc 65 . . . . . . . 8 (𝜑 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩)
4140eleq1d 2826 . . . . . . 7 (𝜑 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) ↔ ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤)))
4241adantr 480 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) ↔ ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤)))
433ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷))
44 simplrl 777 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → 𝑣𝐾)
45 simprl 771 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣)
46 cnpimaex 23264 . . . . . . . . . 10 (((𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷) ∧ 𝑣𝐾 ∧ ((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣) → ∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣))
4743, 44, 45, 46syl3anc 1373 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣))
488ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷))
49 simplrr 778 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → 𝑤𝐿)
50 simprr 773 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)
51 cnpimaex 23264 . . . . . . . . . 10 (((𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷) ∧ 𝑤𝐿 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤) → ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))
5248, 49, 50, 51syl3anc 1373 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))
5347, 52jca 511 . . . . . . . 8 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
5453ex 412 . . . . . . 7 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → ((((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤) → (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
55 opelxp 5721 . . . . . . 7 (⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤) ↔ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤))
56 reeanv 3229 . . . . . . 7 (∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) ↔ (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
5754, 55, 563imtr4g 296 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤) → ∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
5842, 57sylbid 240 . . . . 5 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
59 an4 656 . . . . . . . . . . 11 (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) ↔ ((𝐷𝑟𝐷𝑠) ∧ (((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
60 elin 3967 . . . . . . . . . . . . . 14 (𝐷 ∈ (𝑟𝑠) ↔ (𝐷𝑟𝐷𝑠))
6160biimpri 228 . . . . . . . . . . . . 13 ((𝐷𝑟𝐷𝑠) → 𝐷 ∈ (𝑟𝑠))
6261a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((𝐷𝑟𝐷𝑠) → 𝐷 ∈ (𝑟𝑠)))
63 simpl 482 . . . . . . . . . . . . . . . 16 ((𝑟𝐽𝑠𝐽) → 𝑟𝐽)
64 toponss 22933 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑟𝐽) → 𝑟𝑋)
651, 63, 64syl2an 596 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → 𝑟𝑋)
66 ssinss1 4246 . . . . . . . . . . . . . . . . . . . . 21 (𝑟𝑋 → (𝑟𝑠) ⊆ 𝑋)
6766adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑟𝑋) → (𝑟𝑠) ⊆ 𝑋)
6867sselda 3983 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑋)
6928ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
70 nffvmpt1 6917 . . . . . . . . . . . . . . . . . . . . 21 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡)
71 nffvmpt1 6917 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑥𝑋𝐴)‘𝑡)
72 nffvmpt1 6917 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑥𝑋𝐵)‘𝑡)
7371, 72nfop 4889 . . . . . . . . . . . . . . . . . . . . 21 𝑥⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩
7470, 73nfeq 2919 . . . . . . . . . . . . . . . . . . . 20 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩
75 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡))
76 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝑡))
77 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → ((𝑥𝑋𝐵)‘𝑥) = ((𝑥𝑋𝐵)‘𝑡))
7876, 77opeq12d 4881 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩)
7975, 78eqeq12d 2753 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑡 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩))
8074, 79rspc 3610 . . . . . . . . . . . . . . . . . . 19 (𝑡𝑋 → (∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩))
8168, 69, 80sylc 65 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩)
82 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ (𝑟𝑠))
8382elin1d 4204 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑟)
845ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑥𝑋𝐴):𝑋𝑌)
8584ffund 6740 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → Fun (𝑥𝑋𝐴))
8667adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ 𝑋)
8784fdmd 6746 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → dom (𝑥𝑋𝐴) = 𝑋)
8886, 87sseqtrrd 4021 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ dom (𝑥𝑋𝐴))
8988, 82sseldd 3984 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ dom (𝑥𝑋𝐴))
90 funfvima 7250 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝑥𝑋𝐴) ∧ 𝑡 ∈ dom (𝑥𝑋𝐴)) → (𝑡𝑟 → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟)))
9185, 89, 90syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑡𝑟 → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟)))
9283, 91mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟))
9382elin2d 4205 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑠)
9410ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑥𝑋𝐵):𝑋𝑍)
9594ffund 6740 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → Fun (𝑥𝑋𝐵))
9694fdmd 6746 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → dom (𝑥𝑋𝐵) = 𝑋)
9786, 96sseqtrrd 4021 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ dom (𝑥𝑋𝐵))
9897, 82sseldd 3984 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ dom (𝑥𝑋𝐵))
99 funfvima 7250 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝑥𝑋𝐵) ∧ 𝑡 ∈ dom (𝑥𝑋𝐵)) → (𝑡𝑠 → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠)))
10095, 98, 99syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑡𝑠 → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠)))
10193, 100mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠))
10292, 101opelxpd 5724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩ ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
10381, 102eqeltrd 2841 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
104103ralrimiva 3146 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑋) → ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
10513ffund 6740 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
106105adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑋) → Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
10713fdmd 6746 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = 𝑋)
108107adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑋) → dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = 𝑋)
10967, 108sseqtrrd 4021 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑋) → (𝑟𝑠) ⊆ dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
110 funimass4 6973 . . . . . . . . . . . . . . . . 17 ((Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) ∧ (𝑟𝑠) ⊆ dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ↔ ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠))))
111106, 109, 110syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑋) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ↔ ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠))))
112104, 111mpbird 257 . . . . . . . . . . . . . . 15 ((𝜑𝑟𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
11365, 112syldan 591 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
114113adantlr 715 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
115 xpss12 5700 . . . . . . . . . . . . 13 ((((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤) → (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ⊆ (𝑣 × 𝑤))
116 sstr2 3990 . . . . . . . . . . . . 13 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) → ((((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ⊆ (𝑣 × 𝑤) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
117114, 115, 116syl2im 40 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
11862, 117anim12d 609 . . . . . . . . . . 11 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟𝐷𝑠) ∧ (((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
11959, 118biimtrid 242 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
120 topontop 22919 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
1211, 120syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ Top)
122 inopn 22905 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑟𝐽𝑠𝐽) → (𝑟𝑠) ∈ 𝐽)
1231223expb 1121 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝑟𝐽𝑠𝐽)) → (𝑟𝑠) ∈ 𝐽)
124121, 123sylan 580 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → (𝑟𝑠) ∈ 𝐽)
125124adantlr 715 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (𝑟𝑠) ∈ 𝐽)
126119, 125jctild 525 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))))
127126expimpd 453 . . . . . . . 8 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑟𝐽𝑠𝐽) ∧ ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))) → ((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))))
128 eleq2 2830 . . . . . . . . . 10 (𝑧 = (𝑟𝑠) → (𝐷𝑧𝐷 ∈ (𝑟𝑠)))
129 imaeq2 6074 . . . . . . . . . . 11 (𝑧 = (𝑟𝑠) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)))
130129sseq1d 4015 . . . . . . . . . 10 (𝑧 = (𝑟𝑠) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤) ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
131128, 130anbi12d 632 . . . . . . . . 9 (𝑧 = (𝑟𝑠) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)) ↔ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
132131rspcev 3622 . . . . . . . 8 (((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))
133127, 132syl6 35 . . . . . . 7 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑟𝐽𝑠𝐽) ∧ ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
134133expd 415 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → ((𝑟𝐽𝑠𝐽) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
135134rexlimdvv 3212 . . . . 5 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
13658, 135syld 47 . . . 4 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
137136ralrimivva 3202 . . 3 (𝜑 → ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
138 vex 3484 . . . . . 6 𝑣 ∈ V
139 vex 3484 . . . . . 6 𝑤 ∈ V
140138, 139xpex 7773 . . . . 5 (𝑣 × 𝑤) ∈ V
141140rgen2w 3066 . . . 4 𝑣𝐾𝑤𝐿 (𝑣 × 𝑤) ∈ V
142 eqid 2737 . . . . 5 (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤)) = (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))
143 eleq2 2830 . . . . . 6 (𝑦 = (𝑣 × 𝑤) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤)))
144 sseq2 4010 . . . . . . . 8 (𝑦 = (𝑣 × 𝑤) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))
145144anbi2d 630 . . . . . . 7 (𝑦 = (𝑣 × 𝑤) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦) ↔ (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
146145rexbidv 3179 . . . . . 6 (𝑦 = (𝑣 × 𝑤) → (∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦) ↔ ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
147143, 146imbi12d 344 . . . . 5 (𝑦 = (𝑣 × 𝑤) → ((((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
148142, 147ralrnmpo 7572 . . . 4 (∀𝑣𝐾𝑤𝐿 (𝑣 × 𝑤) ∈ V → (∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
149141, 148ax-mp 5 . . 3 (∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
150137, 149sylibr 234 . 2 (𝜑 → ∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)))
151 topontop 22919 . . . . 5 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
1522, 151syl 17 . . . 4 (𝜑𝐾 ∈ Top)
153 topontop 22919 . . . . 5 (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top)
1547, 153syl 17 . . . 4 (𝜑𝐿 ∈ Top)
155 eqid 2737 . . . . 5 ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤)) = ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))
156155txval 23572 . . . 4 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐾 ×t 𝐿) = (topGen‘ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))))
157152, 154, 156syl2anc 584 . . 3 (𝜑 → (𝐾 ×t 𝐿) = (topGen‘ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))))
158 txtopon 23599 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑌 × 𝑍)))
1592, 7, 158syl2anc 584 . . 3 (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑌 × 𝑍)))
1601, 157, 159, 14tgcnp 23261 . 2 (𝜑 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) ∈ ((𝐽 CnP (𝐾 ×t 𝐿))‘𝐷) ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩):𝑋⟶(𝑌 × 𝑍) ∧ ∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)))))
16113, 150, 160mpbir2and 713 1 (𝜑 → (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) ∈ ((𝐽 CnP (𝐾 ×t 𝐿))‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3061  wrex 3070  Vcvv 3480  cin 3950  wss 3951  cop 4632  cmpt 5225   × cxp 5683  dom cdm 5685  ran crn 5686  cima 5688  Fun wfun 6555  wf 6557  cfv 6561  (class class class)co 7431  cmpo 7433  topGenctg 17482  Topctop 22899  TopOnctopon 22916   CnP ccnp 23233   ×t ctx 23568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-map 8868  df-topgen 17488  df-top 22900  df-topon 22917  df-bases 22953  df-cnp 23236  df-tx 23570
This theorem is referenced by:  limccnp2  25927
  Copyright terms: Public domain W3C validator