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

Theorem txcnp 22971
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 22601 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷)) → (𝑥𝑋𝐴):𝑋𝑌)
51, 2, 3, 4syl3anc 1371 . . . . 5 (𝜑 → (𝑥𝑋𝐴):𝑋𝑌)
65fvmptelcdm 7061 . . . 4 ((𝜑𝑥𝑋) → 𝐴𝑌)
7 txcnp.6 . . . . . 6 (𝜑𝐿 ∈ (TopOn‘𝑍))
8 txcnp.9 . . . . . 6 (𝜑 → (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷))
9 cnpf2 22601 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷)) → (𝑥𝑋𝐵):𝑋𝑍)
101, 7, 8, 9syl3anc 1371 . . . . 5 (𝜑 → (𝑥𝑋𝐵):𝑋𝑍)
1110fvmptelcdm 7061 . . . 4 ((𝜑𝑥𝑋) → 𝐵𝑍)
126, 11opelxpd 5671 . . 3 ((𝜑𝑥𝑋) → ⟨𝐴, 𝐵⟩ ∈ (𝑌 × 𝑍))
1312fmpttd 7063 . 2 (𝜑 → (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩):𝑋⟶(𝑌 × 𝑍))
14 txcnp.7 . . . . . . . . 9 (𝜑𝐷𝑋)
15 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝑥𝑋)
16 opex 5421 . . . . . . . . . . . 12 𝐴, 𝐵⟩ ∈ V
17 eqid 2736 . . . . . . . . . . . . 13 (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)
1817fvmpt2 6959 . . . . . . . . . . . 12 ((𝑥𝑋 ∧ ⟨𝐴, 𝐵⟩ ∈ V) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨𝐴, 𝐵⟩)
1915, 16, 18sylancl 586 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨𝐴, 𝐵⟩)
20 eqid 2736 . . . . . . . . . . . . . 14 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
2120fvmpt2 6959 . . . . . . . . . . . . 13 ((𝑥𝑋𝐴𝑌) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
2215, 6, 21syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐴)‘𝑥) = 𝐴)
23 eqid 2736 . . . . . . . . . . . . . 14 (𝑥𝑋𝐵) = (𝑥𝑋𝐵)
2423fvmpt2 6959 . . . . . . . . . . . . 13 ((𝑥𝑋𝐵𝑍) → ((𝑥𝑋𝐵)‘𝑥) = 𝐵)
2515, 11, 24syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ((𝑥𝑋𝐵)‘𝑥) = 𝐵)
2622, 25opeq12d 4838 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨𝐴, 𝐵⟩)
2719, 26eqtr4d 2779 . . . . . . . . . 10 ((𝜑𝑥𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
2827ralrimiva 3143 . . . . . . . . 9 (𝜑 → ∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
29 nffvmpt1 6853 . . . . . . . . . . 11 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷)
30 nffvmpt1 6853 . . . . . . . . . . . 12 𝑥((𝑥𝑋𝐴)‘𝐷)
31 nffvmpt1 6853 . . . . . . . . . . . 12 𝑥((𝑥𝑋𝐵)‘𝐷)
3230, 31nfop 4846 . . . . . . . . . . 11 𝑥⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩
3329, 32nfeq 2920 . . . . . . . . . 10 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩
34 fveq2 6842 . . . . . . . . . . 11 (𝑥 = 𝐷 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷))
35 fveq2 6842 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝐷))
36 fveq2 6842 . . . . . . . . . . . 12 (𝑥 = 𝐷 → ((𝑥𝑋𝐵)‘𝑥) = ((𝑥𝑋𝐵)‘𝐷))
3735, 36opeq12d 4838 . . . . . . . . . . 11 (𝑥 = 𝐷 → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩)
3834, 37eqeq12d 2752 . . . . . . . . . 10 (𝑥 = 𝐷 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩))
3933, 38rspc 3569 . . . . . . . . 9 (𝐷𝑋 → (∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩))
4014, 28, 39sylc 65 . . . . . . . 8 (𝜑 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) = ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩)
4140eleq1d 2822 . . . . . . 7 (𝜑 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) ↔ ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤)))
4241adantr 481 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) ↔ ⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤)))
433ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷))
44 simplrl 775 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → 𝑣𝐾)
45 simprl 769 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣)
46 cnpimaex 22607 . . . . . . . . . 10 (((𝑥𝑋𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷) ∧ 𝑣𝐾 ∧ ((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣) → ∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣))
4743, 44, 45, 46syl3anc 1371 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣))
488ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷))
49 simplrr 776 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → 𝑤𝐿)
50 simprr 771 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)
51 cnpimaex 22607 . . . . . . . . . 10 (((𝑥𝑋𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷) ∧ 𝑤𝐿 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤) → ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))
5248, 49, 50, 51syl3anc 1371 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))
5347, 52jca 512 . . . . . . . 8 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤)) → (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
5453ex 413 . . . . . . 7 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → ((((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤) → (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
55 opelxp 5669 . . . . . . 7 (⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤) ↔ (((𝑥𝑋𝐴)‘𝐷) ∈ 𝑣 ∧ ((𝑥𝑋𝐵)‘𝐷) ∈ 𝑤))
56 reeanv 3217 . . . . . . 7 (∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) ↔ (∃𝑟𝐽 (𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ ∃𝑠𝐽 (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
5754, 55, 563imtr4g 295 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (⟨((𝑥𝑋𝐴)‘𝐷), ((𝑥𝑋𝐵)‘𝐷)⟩ ∈ (𝑣 × 𝑤) → ∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
5842, 57sylbid 239 . . . . 5 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))))
59 an4 654 . . . . . . . . . . 11 (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) ↔ ((𝐷𝑟𝐷𝑠) ∧ (((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)))
60 elin 3926 . . . . . . . . . . . . . 14 (𝐷 ∈ (𝑟𝑠) ↔ (𝐷𝑟𝐷𝑠))
6160biimpri 227 . . . . . . . . . . . . 13 ((𝐷𝑟𝐷𝑠) → 𝐷 ∈ (𝑟𝑠))
6261a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((𝐷𝑟𝐷𝑠) → 𝐷 ∈ (𝑟𝑠)))
63 simpl 483 . . . . . . . . . . . . . . . 16 ((𝑟𝐽𝑠𝐽) → 𝑟𝐽)
64 toponss 22276 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑟𝐽) → 𝑟𝑋)
651, 63, 64syl2an 596 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → 𝑟𝑋)
66 ssinss1 4197 . . . . . . . . . . . . . . . . . . . . 21 (𝑟𝑋 → (𝑟𝑠) ⊆ 𝑋)
6766adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑟𝑋) → (𝑟𝑠) ⊆ 𝑋)
6867sselda 3944 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑋)
6928ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩)
70 nffvmpt1 6853 . . . . . . . . . . . . . . . . . . . . 21 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡)
71 nffvmpt1 6853 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑥𝑋𝐴)‘𝑡)
72 nffvmpt1 6853 . . . . . . . . . . . . . . . . . . . . . 22 𝑥((𝑥𝑋𝐵)‘𝑡)
7371, 72nfop 4846 . . . . . . . . . . . . . . . . . . . . 21 𝑥⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩
7470, 73nfeq 2920 . . . . . . . . . . . . . . . . . . . 20 𝑥((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩
75 fveq2 6842 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡))
76 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → ((𝑥𝑋𝐴)‘𝑥) = ((𝑥𝑋𝐴)‘𝑡))
77 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → ((𝑥𝑋𝐵)‘𝑥) = ((𝑥𝑋𝐵)‘𝑡))
7876, 77opeq12d 4838 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩)
7975, 78eqeq12d 2752 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑡 → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩))
8074, 79rspc 3569 . . . . . . . . . . . . . . . . . . 19 (𝑡𝑋 → (∀𝑥𝑋 ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑥) = ⟨((𝑥𝑋𝐴)‘𝑥), ((𝑥𝑋𝐵)‘𝑥)⟩ → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩))
8168, 69, 80sylc 65 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) = ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩)
82 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ (𝑟𝑠))
8382elin1d 4158 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑟)
845ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑥𝑋𝐴):𝑋𝑌)
8584ffund 6672 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → Fun (𝑥𝑋𝐴))
8667adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ 𝑋)
8784fdmd 6679 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → dom (𝑥𝑋𝐴) = 𝑋)
8886, 87sseqtrrd 3985 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ dom (𝑥𝑋𝐴))
8988, 82sseldd 3945 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ dom (𝑥𝑋𝐴))
90 funfvima 7180 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝑥𝑋𝐴) ∧ 𝑡 ∈ dom (𝑥𝑋𝐴)) → (𝑡𝑟 → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟)))
9185, 89, 90syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑡𝑟 → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟)))
9283, 91mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋𝐴)‘𝑡) ∈ ((𝑥𝑋𝐴) “ 𝑟))
9382elin2d 4159 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡𝑠)
9410ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑥𝑋𝐵):𝑋𝑍)
9594ffund 6672 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → Fun (𝑥𝑋𝐵))
9694fdmd 6679 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → dom (𝑥𝑋𝐵) = 𝑋)
9786, 96sseqtrrd 3985 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑟𝑠) ⊆ dom (𝑥𝑋𝐵))
9897, 82sseldd 3945 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → 𝑡 ∈ dom (𝑥𝑋𝐵))
99 funfvima 7180 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝑥𝑋𝐵) ∧ 𝑡 ∈ dom (𝑥𝑋𝐵)) → (𝑡𝑠 → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠)))
10095, 98, 99syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → (𝑡𝑠 → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠)))
10193, 100mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋𝐵)‘𝑡) ∈ ((𝑥𝑋𝐵) “ 𝑠))
10292, 101opelxpd 5671 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ⟨((𝑥𝑋𝐴)‘𝑡), ((𝑥𝑋𝐵)‘𝑡)⟩ ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
10381, 102eqeltrd 2838 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟𝑋) ∧ 𝑡 ∈ (𝑟𝑠)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
104103ralrimiva 3143 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑋) → ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
10513ffund 6672 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
106105adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑋) → Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
10713fdmd 6679 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = 𝑋)
108107adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑟𝑋) → dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) = 𝑋)
10967, 108sseqtrrd 3985 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟𝑋) → (𝑟𝑠) ⊆ dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩))
110 funimass4 6907 . . . . . . . . . . . . . . . . 17 ((Fun (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) ∧ (𝑟𝑠) ⊆ dom (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ↔ ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠))))
111106, 109, 110syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑟𝑋) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ↔ ∀𝑡 ∈ (𝑟𝑠)((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝑡) ∈ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠))))
112104, 111mpbird 256 . . . . . . . . . . . . . . 15 ((𝜑𝑟𝑋) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
11365, 112syldan 591 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
114113adantlr 713 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)))
115 xpss12 5648 . . . . . . . . . . . . 13 ((((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤) → (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ⊆ (𝑣 × 𝑤))
116 sstr2 3951 . . . . . . . . . . . . 13 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) → ((((𝑥𝑋𝐴) “ 𝑟) × ((𝑥𝑋𝐵) “ 𝑠)) ⊆ (𝑣 × 𝑤) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
117114, 115, 116syl2im 40 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → ((((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
11862, 117anim12d 609 . . . . . . . . . . 11 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟𝐷𝑠) ∧ (((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
11959, 118biimtrid 241 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
120 topontop 22262 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
1211, 120syl 17 . . . . . . . . . . . 12 (𝜑𝐽 ∈ Top)
122 inopn 22248 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑟𝐽𝑠𝐽) → (𝑟𝑠) ∈ 𝐽)
1231223expb 1120 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝑟𝐽𝑠𝐽)) → (𝑟𝑠) ∈ 𝐽)
124121, 123sylan 580 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝐽𝑠𝐽)) → (𝑟𝑠) ∈ 𝐽)
125124adantlr 713 . . . . . . . . . 10 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (𝑟𝑠) ∈ 𝐽)
126119, 125jctild 526 . . . . . . . . 9 (((𝜑 ∧ (𝑣𝐾𝑤𝐿)) ∧ (𝑟𝐽𝑠𝐽)) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))))
127126expimpd 454 . . . . . . . 8 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑟𝐽𝑠𝐽) ∧ ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))) → ((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))))
128 eleq2 2826 . . . . . . . . . 10 (𝑧 = (𝑟𝑠) → (𝐷𝑧𝐷 ∈ (𝑟𝑠)))
129 imaeq2 6009 . . . . . . . . . . 11 (𝑧 = (𝑟𝑠) → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) = ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)))
130129sseq1d 3975 . . . . . . . . . 10 (𝑧 = (𝑟𝑠) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤) ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤)))
131128, 130anbi12d 631 . . . . . . . . 9 (𝑧 = (𝑟𝑠) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)) ↔ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))))
132131rspcev 3581 . . . . . . . 8 (((𝑟𝑠) ∈ 𝐽 ∧ (𝐷 ∈ (𝑟𝑠) ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ (𝑟𝑠)) ⊆ (𝑣 × 𝑤))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))
133127, 132syl6 35 . . . . . . 7 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑟𝐽𝑠𝐽) ∧ ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
134133expd 416 . . . . . 6 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → ((𝑟𝐽𝑠𝐽) → (((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
135134rexlimdvv 3204 . . . . 5 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (∃𝑟𝐽𝑠𝐽 ((𝐷𝑟 ∧ ((𝑥𝑋𝐴) “ 𝑟) ⊆ 𝑣) ∧ (𝐷𝑠 ∧ ((𝑥𝑋𝐵) “ 𝑠) ⊆ 𝑤)) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
13658, 135syld 47 . . . 4 ((𝜑 ∧ (𝑣𝐾𝑤𝐿)) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
137136ralrimivva 3197 . . 3 (𝜑 → ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
138 vex 3449 . . . . . 6 𝑣 ∈ V
139 vex 3449 . . . . . 6 𝑤 ∈ V
140138, 139xpex 7687 . . . . 5 (𝑣 × 𝑤) ∈ V
141140rgen2w 3069 . . . 4 𝑣𝐾𝑤𝐿 (𝑣 × 𝑤) ∈ V
142 eqid 2736 . . . . 5 (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤)) = (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))
143 eleq2 2826 . . . . . 6 (𝑦 = (𝑣 × 𝑤) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤)))
144 sseq2 3970 . . . . . . . 8 (𝑦 = (𝑣 × 𝑤) → (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))
145144anbi2d 629 . . . . . . 7 (𝑦 = (𝑣 × 𝑤) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦) ↔ (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
146145rexbidv 3175 . . . . . 6 (𝑦 = (𝑣 × 𝑤) → (∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦) ↔ ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
147143, 146imbi12d 344 . . . . 5 (𝑦 = (𝑣 × 𝑤) → ((((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
148142, 147ralrnmpo 7494 . . . 4 (∀𝑣𝐾𝑤𝐿 (𝑣 × 𝑤) ∈ V → (∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤)))))
149141, 148ax-mp 5 . . 3 (∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)) ↔ ∀𝑣𝐾𝑤𝐿 (((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ (𝑣 × 𝑤) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ (𝑣 × 𝑤))))
150137, 149sylibr 233 . 2 (𝜑 → ∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)))
151 topontop 22262 . . . . 5 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
1522, 151syl 17 . . . 4 (𝜑𝐾 ∈ Top)
153 topontop 22262 . . . . 5 (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top)
1547, 153syl 17 . . . 4 (𝜑𝐿 ∈ Top)
155 eqid 2736 . . . . 5 ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤)) = ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))
156155txval 22915 . . . 4 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐾 ×t 𝐿) = (topGen‘ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))))
157152, 154, 156syl2anc 584 . . 3 (𝜑 → (𝐾 ×t 𝐿) = (topGen‘ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))))
158 txtopon 22942 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑌 × 𝑍)))
1592, 7, 158syl2anc 584 . . 3 (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑌 × 𝑍)))
1601, 157, 159, 14tgcnp 22604 . 2 (𝜑 → ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) ∈ ((𝐽 CnP (𝐾 ×t 𝐿))‘𝐷) ↔ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩):𝑋⟶(𝑌 × 𝑍) ∧ ∀𝑦 ∈ ran (𝑣𝐾, 𝑤𝐿 ↦ (𝑣 × 𝑤))(((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)‘𝐷) ∈ 𝑦 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) “ 𝑧) ⊆ 𝑦)))))
16113, 150, 160mpbir2and 711 1 (𝜑 → (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩) ∈ ((𝐽 CnP (𝐾 ×t 𝐿))‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3064  wrex 3073  Vcvv 3445  cin 3909  wss 3910  cop 4592  cmpt 5188   × cxp 5631  dom cdm 5633  ran crn 5634  cima 5636  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  topGenctg 17319  Topctop 22242  TopOnctopon 22259   CnP ccnp 22576   ×t ctx 22911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767  df-topgen 17325  df-top 22243  df-topon 22260  df-bases 22296  df-cnp 22579  df-tx 22913
This theorem is referenced by:  limccnp2  25256
  Copyright terms: Public domain W3C validator