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

Theorem txlm 12488
 Description: Two sequences converge iff the sequence of their ordered pairs converges. Proposition 14-2.6 of [Gleason] p. 230. (Contributed by NM, 16-Jul-2007.) (Revised by Mario Carneiro, 5-May-2014.)
Hypotheses
Ref Expression
txlm.z 𝑍 = (ℤ𝑀)
txlm.m (𝜑𝑀 ∈ ℤ)
txlm.j (𝜑𝐽 ∈ (TopOn‘𝑋))
txlm.k (𝜑𝐾 ∈ (TopOn‘𝑌))
txlm.f (𝜑𝐹:𝑍𝑋)
txlm.g (𝜑𝐺:𝑍𝑌)
txlm.h 𝐻 = (𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
Assertion
Ref Expression
txlm (𝜑 → ((𝐹(⇝𝑡𝐽)𝑅𝐺(⇝𝑡𝐾)𝑆) ↔ 𝐻(⇝𝑡‘(𝐽 ×t 𝐾))⟨𝑅, 𝑆⟩))
Distinct variable groups:   𝑛,𝐹   𝜑,𝑛   𝑛,𝐺   𝑛,𝐽   𝑛,𝐾   𝑛,𝑋   𝑛,𝑌   𝑛,𝑍
Allowed substitution hints:   𝑅(𝑛)   𝑆(𝑛)   𝐻(𝑛)   𝑀(𝑛)

Proof of Theorem txlm
Dummy variables 𝑗 𝑘 𝑢 𝑣 𝑤 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r19.27v 2562 . . . . . . . 8 ((∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∀𝑢𝐽 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
2 r19.28v 2563 . . . . . . . . 9 (((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∀𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
32ralimi 2498 . . . . . . . 8 (∀𝑢𝐽 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∀𝑢𝐽𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
41, 3syl 14 . . . . . . 7 ((∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∀𝑢𝐽𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
5 simprl 521 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ ⟨𝑅, 𝑆⟩ ∈ 𝑤)) → 𝑤 ∈ (𝐽 ×t 𝐾))
6 txlm.j . . . . . . . . . . . . . . . . . 18 (𝜑𝐽 ∈ (TopOn‘𝑋))
7 topontop 12221 . . . . . . . . . . . . . . . . . 18 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
86, 7syl 14 . . . . . . . . . . . . . . . . 17 (𝜑𝐽 ∈ Top)
9 txlm.k . . . . . . . . . . . . . . . . . 18 (𝜑𝐾 ∈ (TopOn‘𝑌))
10 topontop 12221 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
119, 10syl 14 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ Top)
12 eqid 2140 . . . . . . . . . . . . . . . . . 18 ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
1312txval 12464 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
148, 11, 13syl2anc 409 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
1514adantr 274 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ ⟨𝑅, 𝑆⟩ ∈ 𝑤)) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
165, 15eleqtrd 2219 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ ⟨𝑅, 𝑆⟩ ∈ 𝑤)) → 𝑤 ∈ (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
17 simprr 522 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ ⟨𝑅, 𝑆⟩ ∈ 𝑤)) → ⟨𝑅, 𝑆⟩ ∈ 𝑤)
18 tg2 12269 . . . . . . . . . . . . . 14 ((𝑤 ∈ (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) ∧ ⟨𝑅, 𝑆⟩ ∈ 𝑤) → ∃𝑡 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑡𝑡𝑤))
1916, 17, 18syl2anc 409 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ ⟨𝑅, 𝑆⟩ ∈ 𝑤)) → ∃𝑡 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑡𝑡𝑤))
20 vex 2692 . . . . . . . . . . . . . . . 16 𝑢 ∈ V
21 vex 2692 . . . . . . . . . . . . . . . 16 𝑣 ∈ V
2220, 21xpex 4662 . . . . . . . . . . . . . . 15 (𝑢 × 𝑣) ∈ V
2322rgen2w 2491 . . . . . . . . . . . . . 14 𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V
24 eqid 2140 . . . . . . . . . . . . . . 15 (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
25 eleq2 2204 . . . . . . . . . . . . . . . 16 (𝑡 = (𝑢 × 𝑣) → (⟨𝑅, 𝑆⟩ ∈ 𝑡 ↔ ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣)))
26 sseq1 3125 . . . . . . . . . . . . . . . 16 (𝑡 = (𝑢 × 𝑣) → (𝑡𝑤 ↔ (𝑢 × 𝑣) ⊆ 𝑤))
2725, 26anbi12d 465 . . . . . . . . . . . . . . 15 (𝑡 = (𝑢 × 𝑣) → ((⟨𝑅, 𝑆⟩ ∈ 𝑡𝑡𝑤) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)))
2824, 27rexrnmpo 5894 . . . . . . . . . . . . . 14 (∀𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V → (∃𝑡 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑡𝑡𝑤) ↔ ∃𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)))
2923, 28ax-mp 5 . . . . . . . . . . . . 13 (∃𝑡 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑡𝑡𝑤) ↔ ∃𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))
3019, 29sylib 121 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ ⟨𝑅, 𝑆⟩ ∈ 𝑤)) → ∃𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))
3130ex 114 . . . . . . . . . . 11 (𝜑 → ((𝑤 ∈ (𝐽 ×t 𝐾) ∧ ⟨𝑅, 𝑆⟩ ∈ 𝑤) → ∃𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)))
32 r19.29 2572 . . . . . . . . . . . . 13 ((∀𝑢𝐽𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ∧ ∃𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑢𝐽 (∀𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ∧ ∃𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)))
33 r19.29 2572 . . . . . . . . . . . . . . 15 ((∀𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ∧ ∃𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑣𝐾 (((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)))
34 simprl 521 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣))
35 opelxp 4577 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑅𝑢𝑆𝑣))
3634, 35sylib 121 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → (𝑅𝑢𝑆𝑣))
37 pm2.27 40 . . . . . . . . . . . . . . . . . . . . 21 (𝑅𝑢 → ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢))
38 pm2.27 40 . . . . . . . . . . . . . . . . . . . . 21 (𝑆𝑣 → ((𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))
3937, 38im2anan9 588 . . . . . . . . . . . . . . . . . . . 20 ((𝑅𝑢𝑆𝑣) → (((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢 ∧ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
4036, 39syl 14 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → (((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢 ∧ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
41 txlm.z . . . . . . . . . . . . . . . . . . . . 21 𝑍 = (ℤ𝑀)
4241rexanuz2 10796 . . . . . . . . . . . . . . . . . . . 20 (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ 𝑢 ∧ (𝐺𝑘) ∈ 𝑣) ↔ (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢 ∧ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))
4341uztrn2 9368 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
44 opelxpi 4579 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑘) ∈ 𝑢 ∧ (𝐺𝑘) ∈ 𝑣) → ⟨(𝐹𝑘), (𝐺𝑘)⟩ ∈ (𝑢 × 𝑣))
45 txlm.h . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝐻 = (𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
46 fveq2 5429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
47 fveq2 5429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → (𝐺𝑛) = (𝐺𝑘))
4846, 47opeq12d 3721 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ⟨(𝐹𝑛), (𝐺𝑛)⟩ = ⟨(𝐹𝑘), (𝐺𝑘)⟩)
49 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → 𝑘𝑍)
50 txlm.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝐹:𝑍𝑋)
5150ad4antr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → 𝐹:𝑍𝑋)
5251, 49ffvelrnd 5564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ 𝑋)
53 txlm.g . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝐺:𝑍𝑌)
5453ad4antr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → 𝐺:𝑍𝑌)
5554, 49ffvelrnd 5564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → (𝐺𝑘) ∈ 𝑌)
56 opexg 4158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹𝑘) ∈ 𝑋 ∧ (𝐺𝑘) ∈ 𝑌) → ⟨(𝐹𝑘), (𝐺𝑘)⟩ ∈ V)
5752, 55, 56syl2anc 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → ⟨(𝐹𝑘), (𝐺𝑘)⟩ ∈ V)
5845, 48, 49, 57fvmptd3 5522 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → (𝐻𝑘) = ⟨(𝐹𝑘), (𝐺𝑘)⟩)
5958eleq1d 2209 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → ((𝐻𝑘) ∈ (𝑢 × 𝑣) ↔ ⟨(𝐹𝑘), (𝐺𝑘)⟩ ∈ (𝑢 × 𝑣)))
6044, 59syl5ibr 155 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → (((𝐹𝑘) ∈ 𝑢 ∧ (𝐺𝑘) ∈ 𝑣) → (𝐻𝑘) ∈ (𝑢 × 𝑣)))
61 simplrr 526 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → (𝑢 × 𝑣) ⊆ 𝑤)
6261sseld 3101 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → ((𝐻𝑘) ∈ (𝑢 × 𝑣) → (𝐻𝑘) ∈ 𝑤))
6360, 62syld 45 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘𝑍) → (((𝐹𝑘) ∈ 𝑢 ∧ (𝐺𝑘) ∈ 𝑣) → (𝐻𝑘) ∈ 𝑤))
6443, 63sylan2 284 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (((𝐹𝑘) ∈ 𝑢 ∧ (𝐺𝑘) ∈ 𝑣) → (𝐻𝑘) ∈ 𝑤))
6564anassrs 398 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (((𝐹𝑘) ∈ 𝑢 ∧ (𝐺𝑘) ∈ 𝑣) → (𝐻𝑘) ∈ 𝑤))
6665ralimdva 2502 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ 𝑢 ∧ (𝐺𝑘) ∈ 𝑣) → ∀𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))
6766reximdva 2537 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ 𝑢 ∧ (𝐺𝑘) ∈ 𝑣) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))
6842, 67syl5bir 152 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ((∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢 ∧ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))
6940, 68syld 45 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢𝐽) ∧ 𝑣𝐾) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → (((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))
7069ex 114 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢𝐽) ∧ 𝑣𝐾) → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → (((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
7170impcomd 253 . . . . . . . . . . . . . . . 16 (((𝜑𝑢𝐽) ∧ 𝑣𝐾) → ((((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))
7271rexlimdva 2552 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝐽) → (∃𝑣𝐾 (((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ∧ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))
7333, 72syl5 32 . . . . . . . . . . . . . 14 ((𝜑𝑢𝐽) → ((∀𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ∧ ∃𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))
7473rexlimdva 2552 . . . . . . . . . . . . 13 (𝜑 → (∃𝑢𝐽 (∀𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ∧ ∃𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))
7532, 74syl5 32 . . . . . . . . . . . 12 (𝜑 → ((∀𝑢𝐽𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ∧ ∃𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))
7675expcomd 1418 . . . . . . . . . . 11 (𝜑 → (∃𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → (∀𝑢𝐽𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
7731, 76syld 45 . . . . . . . . . 10 (𝜑 → ((𝑤 ∈ (𝐽 ×t 𝐾) ∧ ⟨𝑅, 𝑆⟩ ∈ 𝑤) → (∀𝑢𝐽𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
7877expdimp 257 . . . . . . . . 9 ((𝜑𝑤 ∈ (𝐽 ×t 𝐾)) → (⟨𝑅, 𝑆⟩ ∈ 𝑤 → (∀𝑢𝐽𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
7978com23 78 . . . . . . . 8 ((𝜑𝑤 ∈ (𝐽 ×t 𝐾)) → (∀𝑢𝐽𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → (⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
8079ralrimdva 2515 . . . . . . 7 (𝜑 → (∀𝑢𝐽𝑣𝐾 ((𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
814, 80syl5 32 . . . . . 6 (𝜑 → ((∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
8281adantr 274 . . . . 5 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → ((∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) → ∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
838adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → 𝐽 ∈ Top)
8411adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → 𝐾 ∈ Top)
85 simprr 522 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → 𝑢𝐽)
86 toponmax 12232 . . . . . . . . . . . . . 14 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
879, 86syl 14 . . . . . . . . . . . . 13 (𝜑𝑌𝐾)
8887adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → 𝑌𝐾)
89 txopn 12474 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑢𝐽𝑌𝐾)) → (𝑢 × 𝑌) ∈ (𝐽 ×t 𝐾))
9083, 84, 85, 88, 89syl22anc 1218 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → (𝑢 × 𝑌) ∈ (𝐽 ×t 𝐾))
91 eleq2 2204 . . . . . . . . . . . . 13 (𝑤 = (𝑢 × 𝑌) → (⟨𝑅, 𝑆⟩ ∈ 𝑤 ↔ ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑌)))
92 eleq2 2204 . . . . . . . . . . . . . 14 (𝑤 = (𝑢 × 𝑌) → ((𝐻𝑘) ∈ 𝑤 ↔ (𝐻𝑘) ∈ (𝑢 × 𝑌)))
9392rexralbidv 2464 . . . . . . . . . . . . 13 (𝑤 = (𝑢 × 𝑌) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑢 × 𝑌)))
9491, 93imbi12d 233 . . . . . . . . . . . 12 (𝑤 = (𝑢 × 𝑌) → ((⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑢 × 𝑌))))
9594rspcv 2789 . . . . . . . . . . 11 ((𝑢 × 𝑌) ∈ (𝐽 ×t 𝐾) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑢 × 𝑌))))
9690, 95syl 14 . . . . . . . . . 10 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑢 × 𝑌))))
97 simprl 521 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → 𝑆𝑌)
98 opelxpi 4579 . . . . . . . . . . . . 13 ((𝑅𝑢𝑆𝑌) → ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑌))
9997, 98sylan2 284 . . . . . . . . . . . 12 ((𝑅𝑢 ∧ (𝜑 ∧ (𝑆𝑌𝑢𝐽))) → ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑌))
10099expcom 115 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → (𝑅𝑢 → ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑌)))
101 simpr 109 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → 𝑘𝑍)
10250ffvelrnda 5563 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ 𝑋)
10353ffvelrnda 5563 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝑌)
104102, 103, 56syl2anc 409 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → ⟨(𝐹𝑘), (𝐺𝑘)⟩ ∈ V)
10545, 48, 101, 104fvmptd3 5522 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑍) → (𝐻𝑘) = ⟨(𝐹𝑘), (𝐺𝑘)⟩)
106105eleq1d 2209 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → ((𝐻𝑘) ∈ (𝑢 × 𝑌) ↔ ⟨(𝐹𝑘), (𝐺𝑘)⟩ ∈ (𝑢 × 𝑌)))
107 opelxp1 4581 . . . . . . . . . . . . . . . . 17 (⟨(𝐹𝑘), (𝐺𝑘)⟩ ∈ (𝑢 × 𝑌) → (𝐹𝑘) ∈ 𝑢)
108106, 107syl6bi 162 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑍) → ((𝐻𝑘) ∈ (𝑢 × 𝑌) → (𝐹𝑘) ∈ 𝑢))
10943, 108sylan2 284 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((𝐻𝑘) ∈ (𝑢 × 𝑌) → (𝐹𝑘) ∈ 𝑢))
110109anassrs 398 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝐻𝑘) ∈ (𝑢 × 𝑌) → (𝐹𝑘) ∈ 𝑢))
111110ralimdva 2502 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑢 × 𝑌) → ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢))
112111reximdva 2537 . . . . . . . . . . . 12 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑢 × 𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢))
113112adantr 274 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑢 × 𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢))
114100, 113imim12d 74 . . . . . . . . . 10 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑌) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑢 × 𝑌)) → (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
11596, 114syld 45 . . . . . . . . 9 ((𝜑 ∧ (𝑆𝑌𝑢𝐽)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
116115anassrs 398 . . . . . . . 8 (((𝜑𝑆𝑌) ∧ 𝑢𝐽) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
117116ralrimdva 2515 . . . . . . 7 ((𝜑𝑆𝑌) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → ∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
118117adantrl 470 . . . . . 6 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → ∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)))
1198adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → 𝐽 ∈ Top)
12011adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → 𝐾 ∈ Top)
121 toponmax 12232 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
1226, 121syl 14 . . . . . . . . . . . . 13 (𝜑𝑋𝐽)
123122adantr 274 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → 𝑋𝐽)
124 simprr 522 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → 𝑣𝐾)
125 txopn 12474 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑋𝐽𝑣𝐾)) → (𝑋 × 𝑣) ∈ (𝐽 ×t 𝐾))
126119, 120, 123, 124, 125syl22anc 1218 . . . . . . . . . . 11 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → (𝑋 × 𝑣) ∈ (𝐽 ×t 𝐾))
127 eleq2 2204 . . . . . . . . . . . . 13 (𝑤 = (𝑋 × 𝑣) → (⟨𝑅, 𝑆⟩ ∈ 𝑤 ↔ ⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑣)))
128 eleq2 2204 . . . . . . . . . . . . . 14 (𝑤 = (𝑋 × 𝑣) → ((𝐻𝑘) ∈ 𝑤 ↔ (𝐻𝑘) ∈ (𝑋 × 𝑣)))
129128rexralbidv 2464 . . . . . . . . . . . . 13 (𝑤 = (𝑋 × 𝑣) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑋 × 𝑣)))
130127, 129imbi12d 233 . . . . . . . . . . . 12 (𝑤 = (𝑋 × 𝑣) → ((⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑣) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑋 × 𝑣))))
131130rspcv 2789 . . . . . . . . . . 11 ((𝑋 × 𝑣) ∈ (𝐽 ×t 𝐾) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑣) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑋 × 𝑣))))
132126, 131syl 14 . . . . . . . . . 10 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑣) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑋 × 𝑣))))
133 opelxpi 4579 . . . . . . . . . . . . 13 ((𝑅𝑋𝑆𝑣) → ⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑣))
134133ex 114 . . . . . . . . . . . 12 (𝑅𝑋 → (𝑆𝑣 → ⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑣)))
135134ad2antrl 482 . . . . . . . . . . 11 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → (𝑆𝑣 → ⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑣)))
136105eleq1d 2209 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → ((𝐻𝑘) ∈ (𝑋 × 𝑣) ↔ ⟨(𝐹𝑘), (𝐺𝑘)⟩ ∈ (𝑋 × 𝑣)))
137 opelxp2 4582 . . . . . . . . . . . . . . . . 17 (⟨(𝐹𝑘), (𝐺𝑘)⟩ ∈ (𝑋 × 𝑣) → (𝐺𝑘) ∈ 𝑣)
138136, 137syl6bi 162 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑍) → ((𝐻𝑘) ∈ (𝑋 × 𝑣) → (𝐺𝑘) ∈ 𝑣))
13943, 138sylan2 284 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((𝐻𝑘) ∈ (𝑋 × 𝑣) → (𝐺𝑘) ∈ 𝑣))
140139anassrs 398 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝐻𝑘) ∈ (𝑋 × 𝑣) → (𝐺𝑘) ∈ 𝑣))
141140ralimdva 2502 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑋 × 𝑣) → ∀𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))
142141reximdva 2537 . . . . . . . . . . . 12 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑋 × 𝑣) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))
143142adantr 274 . . . . . . . . . . 11 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑋 × 𝑣) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))
144135, 143imim12d 74 . . . . . . . . . 10 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑣) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ (𝑋 × 𝑣)) → (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
145132, 144syld 45 . . . . . . . . 9 ((𝜑 ∧ (𝑅𝑋𝑣𝐾)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
146145anassrs 398 . . . . . . . 8 (((𝜑𝑅𝑋) ∧ 𝑣𝐾) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
147146ralrimdva 2515 . . . . . . 7 ((𝜑𝑅𝑋) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
148147adantrr 471 . . . . . 6 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))
149118, 148jcad 305 . . . . 5 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤) → (∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))))
15082, 149impbid 128 . . . 4 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → ((∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)) ↔ ∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
151150pm5.32da 448 . . 3 (𝜑 → (((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))) ↔ ((𝑅𝑋𝑆𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))))
152 opelxp 4577 . . . 4 (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ↔ (𝑅𝑋𝑆𝑌))
153152anbi1i 454 . . 3 ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)) ↔ ((𝑅𝑋𝑆𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤)))
154151, 153bitr4di 197 . 2 (𝜑 → (((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))))
155 txlm.m . . . . 5 (𝜑𝑀 ∈ ℤ)
156 eqidd 2141 . . . . 5 ((𝜑𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
1576, 41, 155, 50, 156lmbrf 12424 . . . 4 (𝜑 → (𝐹(⇝𝑡𝐽)𝑅 ↔ (𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢))))
158 eqidd 2141 . . . . 5 ((𝜑𝑘𝑍) → (𝐺𝑘) = (𝐺𝑘))
1599, 41, 155, 53, 158lmbrf 12424 . . . 4 (𝜑 → (𝐺(⇝𝑡𝐾)𝑆 ↔ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))))
160157, 159anbi12d 465 . . 3 (𝜑 → ((𝐹(⇝𝑡𝐽)𝑅𝐺(⇝𝑡𝐾)𝑆) ↔ ((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))))
161 an4 576 . . 3 (((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣))))
162160, 161syl6bb 195 . 2 (𝜑 → ((𝐹(⇝𝑡𝐽)𝑅𝐺(⇝𝑡𝐾)𝑆) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐺𝑘) ∈ 𝑣)))))
163 txtopon 12471 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
1646, 9, 163syl2anc 409 . . 3 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
16550ffvelrnda 5563 . . . . 5 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ 𝑋)
16653ffvelrnda 5563 . . . . 5 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ 𝑌)
167165, 166opelxpd 4580 . . . 4 ((𝜑𝑛𝑍) → ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑋 × 𝑌))
168167, 45fmptd 5582 . . 3 (𝜑𝐻:𝑍⟶(𝑋 × 𝑌))
169 eqidd 2141 . . 3 ((𝜑𝑘𝑍) → (𝐻𝑘) = (𝐻𝑘))
170164, 41, 155, 168, 169lmbrf 12424 . 2 (𝜑 → (𝐻(⇝𝑡‘(𝐽 ×t 𝐾))⟨𝑅, 𝑆⟩ ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(⟨𝑅, 𝑆⟩ ∈ 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐻𝑘) ∈ 𝑤))))
171154, 162, 1703bitr4d 219 1 (𝜑 → ((𝐹(⇝𝑡𝐽)𝑅𝐺(⇝𝑡𝐾)𝑆) ↔ 𝐻(⇝𝑡‘(𝐽 ×t 𝐾))⟨𝑅, 𝑆⟩))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  Vcvv 2689   ⊆ wss 3076  ⟨cop 3535   class class class wbr 3937   ↦ cmpt 3997   × cxp 4545  ran crn 4548  ⟶wf 5127  ‘cfv 5131  (class class class)co 5782   ∈ cmpo 5784  ℤcz 9079  ℤ≥cuz 9351  topGenctg 12175  Topctop 12204  TopOnctopon 12217  ⇝𝑡clm 12396   ×t ctx 12461 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4051  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-cnex 7736  ax-resscn 7737  ax-1cn 7738  ax-1re 7739  ax-icn 7740  ax-addcl 7741  ax-addrcl 7742  ax-mulcl 7743  ax-addcom 7745  ax-addass 7747  ax-distr 7749  ax-i2m1 7750  ax-0lt1 7751  ax-0id 7753  ax-rnegex 7754  ax-cnre 7756  ax-pre-ltirr 7757  ax-pre-ltwlin 7758  ax-pre-lttrn 7759  ax-pre-apti 7760  ax-pre-ltadd 7761 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-if 3480  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-iun 3823  df-br 3938  df-opab 3998  df-mpt 3999  df-id 4223  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-riota 5738  df-ov 5785  df-oprab 5786  df-mpo 5787  df-1st 6046  df-2nd 6047  df-pm 6553  df-pnf 7827  df-mnf 7828  df-xr 7829  df-ltxr 7830  df-le 7831  df-sub 7960  df-neg 7961  df-inn 8746  df-n0 9003  df-z 9080  df-uz 9352  df-topgen 12181  df-top 12205  df-topon 12218  df-bases 12250  df-lm 12399  df-tx 12462 This theorem is referenced by:  lmcn2  12489
 Copyright terms: Public domain W3C validator