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

Theorem txcnp 23643
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 23273 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷)) → (𝑥𝑋𝐴):𝑋𝑌)
51, 2, 3, 4syl3anc 1370 . . . . 5 (𝜑 → (𝑥𝑋𝐴):𝑋𝑌)
65fvmptelcdm 7132 . . . 4 ((𝜑𝑥𝑋) → 𝐴𝑌)
7 txcnp.6 . . . . . 6 (𝜑𝐿 ∈ (TopOn‘𝑍))
8 txcnp.9 . . . . . 6 (𝜑 → (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷))
9 cnpf2 23273 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷)) → (𝑥𝑋𝐵):𝑋𝑍)
101, 7, 8, 9syl3anc 1370 . . . . 5 (𝜑 → (𝑥𝑋𝐵):𝑋𝑍)
1110fvmptelcdm 7132 . . . 4 ((𝜑𝑥𝑋) → 𝐵𝑍)
126, 11opelxpd 5727 . . 3 ((𝜑𝑥𝑋) → ⟨𝐴, 𝐵⟩ ∈ (𝑌 × 𝑍))
1312fmpttd 7134 . 2 (𝜑 → (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩):𝑋⟶(𝑌 × 𝑍))
14 txcnp.7 . . . . . . . . 9 (𝜑𝐷𝑋)
15 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝑥𝑋)
16 opex 5474 . . . . . . . . . . . 12 𝐴, 𝐵⟩ ∈ V
17 eqid 2734 . . . . . . . . . . . . 13 (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)
1817fvmpt2 7026 . . . . . . . . . . . 12 ((𝑥𝑋 ∧ ⟨𝐴, 𝐵⟩ ∈ V) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨𝐴, 𝐵⟩)
1915, 16, 18sylancl 586 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨𝐴, 𝐵⟩)
20 eqid 2734 . . . . . . . . . . . . . 14 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
2120fvmpt2 7026 . . . . . . . . . . . . 13 ((𝑥𝑋𝐴𝑌) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
2215, 6, 21syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
23 eqid 2734 . . . . . . . . . . . . . 14 (𝑥𝑋𝐵) = (𝑥𝑋𝐵)
2423fvmpt2 7026 . . . . . . . . . . . . 13 ((𝑥𝑋𝐵𝑍) → ((𝑥𝑋𝐵)‘𝑥) = 𝐵)
2515, 11, 24syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐵)‘𝑥) = 𝐵)
2622, 25opeq12d 4885 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨𝐴, 𝐵⟩)
2719, 26eqtr4d 2777 . . . . . . . . . 10 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
2827ralrimiva 3143 . . . . . . . . 9 (𝜑 → ∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
29 nffvmpt1 6917 . . . . . . . . . . 11 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷)
30 nffvmpt1 6917 . . . . . . . . . . . 12 𝑥((𝑥𝑋𝐴)‘𝐷)
31 nffvmpt1 6917 . . . . . . . . . . . 12 𝑥((𝑥𝑋𝐵)‘𝐷)
3230, 31nfop 4893 . . . . . . . . . . 11 𝑥⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩
3329, 32nfeq 2916 . . . . . . . . . 10 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩
34 fveq2 6906 . . . . . . . . . . 11 (𝑥 = 𝐷 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷))
35 fveq2 6906 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝐷))
36 fveq2 6906 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑥𝑋𝐵)‘𝑥) = ((𝑥𝑋𝐵)‘𝐷))
3735, 36opeq12d 4885 . . . . . . . . . . 11 (𝑥 = 𝐷 → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩)
3834, 37eqeq12d 2750 . . . . . . . . . 10 (𝑥 = 𝐷 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩))
3933, 38rspc 3609 . . . . . . . . 9 (𝐷𝑋 → (∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩))
4014, 28, 39sylc 65 . . . . . . . 8 (𝜑 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩)
4140eleq1d 2823 . . . . . . 7 (𝜑 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) ↔ ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤)))
4241adantr 480 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) ↔ ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤)))
433ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷))
44 simplrl 777 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → 𝑣𝐾)
45 simprl 771 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣)
46 cnpimaex 23279 . . . . . . . . . 10 (((𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷) ∧ 𝑣𝐾 ∧ ((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣) → ∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣))
4743, 44, 45, 46syl3anc 1370 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣))
488ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷))
49 simplrr 778 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → 𝑤𝐿)
50 simprr 773 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)
51 cnpimaex 23279 . . . . . . . . . 10 (((𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷) ∧ 𝑤𝐿 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤) → ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))
5248, 49, 50, 51syl3anc 1370 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))
5347, 52jca 511 . . . . . . . 8 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
5453ex 412 . . . . . . 7 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → ((((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤) → (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
55 opelxp 5724 . . . . . . 7 (⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤) ↔ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤))
56 reeanv 3226 . . . . . . 7 (∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) ↔ (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
5754, 55, 563imtr4g 296 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤) → ∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
5842, 57sylbid 240 . . . . 5 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
59 an4 656 . . . . . . . . . . 11 (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) ↔ ((𝐷𝑟𝐷𝑠) ∧ (((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
60 elin 3978 . . . . . . . . . . . . . 14 (𝐷 ∈ (𝑟𝑠) ↔ (𝐷𝑟𝐷𝑠))
6160biimpri 228 . . . . . . . . . . . . 13 ((𝐷𝑟𝐷𝑠) → 𝐷 ∈ (𝑟𝑠))
6261a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((𝐷𝑟𝐷𝑠) → 𝐷 ∈ (𝑟𝑠)))
63 simpl 482 . . . . . . . . . . . . . . . 16 ((𝑟𝐽𝑠𝐽) → 𝑟𝐽)
64 toponss 22948 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑟𝐽) → 𝑟𝑋)
651, 63, 64syl2an 596 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → 𝑟𝑋)
66 ssinss1 4253 . . . . . . . . . . . . . . . . . . . . 21 (𝑟𝑋 → (𝑟𝑠) ⊆ 𝑋)
6766adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑟𝑋) → (𝑟𝑠) ⊆ 𝑋)
6867sselda 3994 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑋)
6928ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
70 nffvmpt1 6917 . . . . . . . . . . . . . . . . . . . . 21 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡)
71 nffvmpt1 6917 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑥𝑋𝐴)‘𝑡)
72 nffvmpt1 6917 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑥𝑋𝐵)‘𝑡)
7371, 72nfop 4893 . . . . . . . . . . . . . . . . . . . . 21 𝑥⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩
7470, 73nfeq 2916 . . . . . . . . . . . . . . . . . . . 20 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩
75 fveq2 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡))
76 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝑡))
77 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → ((𝑥𝑋𝐵)‘𝑥) = ((𝑥𝑋𝐵)‘𝑡))
7876, 77opeq12d 4885 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩)
7975, 78eqeq12d 2750 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑡 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩))
8074, 79rspc 3609 . . . . . . . . . . . . . . . . . . 19 (𝑡𝑋 → (∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩))
8168, 69, 80sylc 65 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩)
82 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ (𝑟𝑠))
8382elin1d 4213 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑟)
845ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑥𝑋𝐴):𝑋𝑌)
8584ffund 6740 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → Fun (𝑥𝑋𝐴))
8667adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ 𝑋)
8784fdmd 6746 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → dom (𝑥𝑋𝐴) = 𝑋)
8886, 87sseqtrrd 4036 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ dom (𝑥𝑋𝐴))
8988, 82sseldd 3995 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ dom (𝑥𝑋𝐴))
90 funfvima 7249 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝑥𝑋𝐴) ∧ 𝑡 ∈ dom (𝑥𝑋𝐴)) → (𝑡𝑟 → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟)))
9185, 89, 90syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑡𝑟 → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟)))
9283, 91mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟))
9382elin2d 4214 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑠)
9410ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑥𝑋𝐵):𝑋𝑍)
9594ffund 6740 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → Fun (𝑥𝑋𝐵))
9694fdmd 6746 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → dom (𝑥𝑋𝐵) = 𝑋)
9786, 96sseqtrrd 4036 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ dom (𝑥𝑋𝐵))
9897, 82sseldd 3995 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ dom (𝑥𝑋𝐵))
99 funfvima 7249 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝑥𝑋𝐵) ∧ 𝑡 ∈ dom (𝑥𝑋𝐵)) → (𝑡𝑠 → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠)))
10095, 98, 99syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑡𝑠 → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠)))
10193, 100mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠))
10292, 101opelxpd 5727 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩ ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
10381, 102eqeltrd 2838 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
104103ralrimiva 3143 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑋) → ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
10513ffund 6740 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
106105adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑋) → Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
10713fdmd 6746 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = 𝑋)
108107adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑋) → dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = 𝑋)
10967, 108sseqtrrd 4036 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑋) → (𝑟𝑠) ⊆ dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
110 funimass4 6972 . . . . . . . . . . . . . . . . 17 ((Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) ∧ (𝑟𝑠) ⊆ dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ↔ ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠))))
111106, 109, 110syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑋) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ↔ ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠))))
112104, 111mpbird 257 . . . . . . . . . . . . . . 15 ((𝜑𝑟𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
11365, 112syldan 591 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
114113adantlr 715 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
115 xpss12 5703 . . . . . . . . . . . . 13 ((((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤) → (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ⊆ (𝑣 × 𝑤))
116 sstr2 4001 . . . . . . . . . . . . 13 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) → ((((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ⊆ (𝑣 × 𝑤) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
117114, 115, 116syl2im 40 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
11862, 117anim12d 609 . . . . . . . . . . 11 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟𝐷𝑠) ∧ (((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
11959, 118biimtrid 242 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
120 topontop 22934 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
1211, 120syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ Top)
122 inopn 22920 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑟𝐽𝑠𝐽) → (𝑟𝑠) ∈ 𝐽)
1231223expb 1119 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝑟𝐽𝑠𝐽)) → (𝑟𝑠) ∈ 𝐽)
124121, 123sylan 580 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → (𝑟𝑠) ∈ 𝐽)
125124adantlr 715 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (𝑟𝑠) ∈ 𝐽)
126119, 125jctild 525 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))))
127126expimpd 453 . . . . . . . 8 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑟𝐽𝑠𝐽) ∧ ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))) → ((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))))
128 eleq2 2827 . . . . . . . . . 10 (𝑧 = (𝑟𝑠) → (𝐷𝑧𝐷 ∈ (𝑟𝑠)))
129 imaeq2 6075 . . . . . . . . . . 11 (𝑧 = (𝑟𝑠) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)))
130129sseq1d 4026 . . . . . . . . . 10 (𝑧 = (𝑟𝑠) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤) ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
131128, 130anbi12d 632 . . . . . . . . 9 (𝑧 = (𝑟𝑠) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)) ↔ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
132131rspcev 3621 . . . . . . . 8 (((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))
133127, 132syl6 35 . . . . . . 7 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑟𝐽𝑠𝐽) ∧ ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
134133expd 415 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → ((𝑟𝐽𝑠𝐽) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
135134rexlimdvv 3209 . . . . 5 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
13658, 135syld 47 . . . 4 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
137136ralrimivva 3199 . . 3 (𝜑 → ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
138 vex 3481 . . . . . 6 𝑣 ∈ V
139 vex 3481 . . . . . 6 𝑤 ∈ V
140138, 139xpex 7771 . . . . 5 (𝑣 × 𝑤) ∈ V
141140rgen2w 3063 . . . 4 𝑣𝐾𝑤𝐿 (𝑣 × 𝑤) ∈ V
142 eqid 2734 . . . . 5 (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤)) = (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))
143 eleq2 2827 . . . . . 6 (𝑦 = (𝑣 × 𝑤) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤)))
144 sseq2 4021 . . . . . . . 8 (𝑦 = (𝑣 × 𝑤) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))
145144anbi2d 630 . . . . . . 7 (𝑦 = (𝑣 × 𝑤) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦) ↔ (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
146145rexbidv 3176 . . . . . 6 (𝑦 = (𝑣 × 𝑤) → (∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦) ↔ ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
147143, 146imbi12d 344 . . . . 5 (𝑦 = (𝑣 × 𝑤) → ((((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
148142, 147ralrnmpo 7571 . . . 4 (∀𝑣𝐾𝑤𝐿 (𝑣 × 𝑤) ∈ V → (∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
149141, 148ax-mp 5 . . 3 (∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
150137, 149sylibr 234 . 2 (𝜑 → ∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)))
151 topontop 22934 . . . . 5 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
1522, 151syl 17 . . . 4 (𝜑𝐾 ∈ Top)
153 topontop 22934 . . . . 5 (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top)
1547, 153syl 17 . . . 4 (𝜑𝐿 ∈ Top)
155 eqid 2734 . . . . 5 ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤)) = ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))
156155txval 23587 . . . 4 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐾 ×t 𝐿) = (topGen‘ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))))
157152, 154, 156syl2anc 584 . . 3 (𝜑 → (𝐾 ×t 𝐿) = (topGen‘ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))))
158 txtopon 23614 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑌 × 𝑍)))
1592, 7, 158syl2anc 584 . . 3 (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑌 × 𝑍)))
1601, 157, 159, 14tgcnp 23276 . 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 1536  wcel 2105  wral 3058  wrex 3067  Vcvv 3477  cin 3961  wss 3962  cop 4636  cmpt 5230   × cxp 5686  dom cdm 5688  ran crn 5689  cima 5691  Fun wfun 6556  wf 6558  cfv 6562  (class class class)co 7430  cmpo 7432  topGenctg 17483  Topctop 22914  TopOnctopon 22931   CnP ccnp 23248   ×t ctx 23583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-map 8866  df-topgen 17489  df-top 22915  df-topon 22932  df-bases 22968  df-cnp 23251  df-tx 23585
This theorem is referenced by:  limccnp2  25941
  Copyright terms: Public domain W3C validator