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

Theorem txflf 21729
Description: Two sequences converge in a filter iff the sequence of their ordered pairs converges. (Contributed by Mario Carneiro, 19-Sep-2015.)
Hypotheses
Ref Expression
txflf.j (𝜑𝐽 ∈ (TopOn‘𝑋))
txflf.k (𝜑𝐾 ∈ (TopOn‘𝑌))
txflf.l (𝜑𝐿 ∈ (Fil‘𝑍))
txflf.f (𝜑𝐹:𝑍𝑋)
txflf.g (𝜑𝐺:𝑍𝑌)
txflf.h 𝐻 = (𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
Assertion
Ref Expression
txflf (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺))))
Distinct variable groups:   𝜑,𝑛   𝑛,𝐹   𝑛,𝐺   𝑛,𝑍   𝑛,𝑋   𝑛,𝑌
Allowed substitution hints:   𝑅(𝑛)   𝑆(𝑛)   𝐻(𝑛)   𝐽(𝑛)   𝐾(𝑛)   𝐿(𝑛)

Proof of Theorem txflf
Dummy variables 𝑢 𝑣 𝑧 𝑓 𝑔 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3192 . . . . . . . 8 𝑢 ∈ V
2 vex 3192 . . . . . . . 8 𝑣 ∈ V
31, 2xpex 6922 . . . . . . 7 (𝑢 × 𝑣) ∈ V
43rgen2w 2920 . . . . . 6 𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V
5 eqid 2621 . . . . . . 7 (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
6 eleq2 2687 . . . . . . . 8 (𝑧 = (𝑢 × 𝑣) → (⟨𝑅, 𝑆⟩ ∈ 𝑧 ↔ ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣)))
7 sseq2 3611 . . . . . . . . 9 (𝑧 = (𝑢 × 𝑣) → ((𝐻) ⊆ 𝑧 ↔ (𝐻) ⊆ (𝑢 × 𝑣)))
87rexbidv 3046 . . . . . . . 8 (𝑧 = (𝑢 × 𝑣) → (∃𝐿 (𝐻) ⊆ 𝑧 ↔ ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)))
96, 8imbi12d 334 . . . . . . 7 (𝑧 = (𝑢 × 𝑣) → ((⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣))))
105, 9ralrnmpt2 6735 . . . . . 6 (∀𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V → (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ ∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣))))
114, 10ax-mp 5 . . . . 5 (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ ∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)))
12 opelxp 5111 . . . . . . . . . . . . . . . 16 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑅𝑢𝑆𝑣))
13 ancom 466 . . . . . . . . . . . . . . . 16 ((𝑅𝑢𝑆𝑣) ↔ (𝑆𝑣𝑅𝑢))
1412, 13bitri 264 . . . . . . . . . . . . . . 15 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑆𝑣𝑅𝑢))
1514a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑆𝑣𝑅𝑢)))
16 r19.40 3081 . . . . . . . . . . . . . . . . 17 (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) → (∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣))
17 raleq 3130 . . . . . . . . . . . . . . . . . . 19 ( = 𝑓 → (∀𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
1817cbvrexv 3163 . . . . . . . . . . . . . . . . . 18 (∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢)
19 raleq 3130 . . . . . . . . . . . . . . . . . . 19 ( = 𝑔 → (∀𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
2019cbvrexv 3163 . . . . . . . . . . . . . . . . . 18 (∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)
2118, 20anbi12i 732 . . . . . . . . . . . . . . . . 17 ((∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
2216, 21sylib 208 . . . . . . . . . . . . . . . 16 (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) → (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
23 reeanv 3100 . . . . . . . . . . . . . . . . 17 (∃𝑓𝐿𝑔𝐿 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
24 txflf.l . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐿 ∈ (Fil‘𝑍))
25 filin 21577 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓𝐿𝑔𝐿) → (𝑓𝑔) ∈ 𝐿)
26253expb 1263 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ (Fil‘𝑍) ∧ (𝑓𝐿𝑔𝐿)) → (𝑓𝑔) ∈ 𝐿)
2724, 26sylan 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓𝐿𝑔𝐿)) → (𝑓𝑔) ∈ 𝐿)
28 inss1 3816 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑔) ⊆ 𝑓
29 ssralv 3650 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑔) ⊆ 𝑓 → (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢))
3028, 29ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢)
31 inss2 3817 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑔) ⊆ 𝑔
32 ssralv 3650 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑔) ⊆ 𝑔 → (∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
3331, 32ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)
3430, 33anim12i 589 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
35 raleq 3130 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑓𝑔) → (∀𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢))
36 raleq 3130 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑓𝑔) → (∀𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
3735, 36anbi12d 746 . . . . . . . . . . . . . . . . . . . . 21 ( = (𝑓𝑔) → ((∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)))
3837rspcev 3298 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝑔) ∈ 𝐿 ∧ (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
3927, 34, 38syl2an 494 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓𝐿𝑔𝐿)) ∧ (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣)) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
4039ex 450 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑓𝐿𝑔𝐿)) → ((∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4140rexlimdvva 3032 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑓𝐿𝑔𝐿 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4223, 41syl5bir 233 . . . . . . . . . . . . . . . 16 (𝜑 → ((∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4322, 42impbid2 216 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)))
44 df-ima 5092 . . . . . . . . . . . . . . . . . . 19 (𝐻) = ran (𝐻)
45 filelss 21575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝐿) → 𝑍)
4624, 45sylan 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐿) → 𝑍)
47 txflf.h . . . . . . . . . . . . . . . . . . . . . . 23 𝐻 = (𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
4847reseq1i 5357 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻) = ((𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ↾ )
49 resmpt 5413 . . . . . . . . . . . . . . . . . . . . . 22 (𝑍 → ((𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ↾ ) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5048, 49syl5eq 2667 . . . . . . . . . . . . . . . . . . . . 21 (𝑍 → (𝐻) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5146, 50syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐿) → (𝐻) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5251rneqd 5318 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐿) → ran (𝐻) = ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5344, 52syl5eq 2667 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐿) → (𝐻) = ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5453sseq1d 3616 . . . . . . . . . . . . . . . . 17 ((𝜑𝐿) → ((𝐻) ⊆ (𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣)))
55 opelxp 5111 . . . . . . . . . . . . . . . . . . 19 (⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣))
5655ralbii 2975 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ∀𝑛 ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣))
57 eqid 2621 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
5857fmpt 6342 . . . . . . . . . . . . . . . . . . 19 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣))
59 opex 4898 . . . . . . . . . . . . . . . . . . . . 21 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ V
6059, 57fnmpti 5984 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) Fn
61 df-f 5856 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣) ↔ ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) Fn ∧ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣)))
6260, 61mpbiran 952 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣))
6358, 62bitri 264 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣))
64 r19.26 3058 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
6556, 63, 643bitr3i 290 . . . . . . . . . . . . . . . . 17 (ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
6654, 65syl6bb 276 . . . . . . . . . . . . . . . 16 ((𝜑𝐿) → ((𝐻) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
6766rexbidva 3043 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣) ↔ ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
68 txflf.f . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹:𝑍𝑋)
6968adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → 𝐹:𝑍𝑋)
70 ffun 6010 . . . . . . . . . . . . . . . . . . 19 (𝐹:𝑍𝑋 → Fun 𝐹)
7169, 70syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝐿) → Fun 𝐹)
72 filelss 21575 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓𝐿) → 𝑓𝑍)
7324, 72sylan 488 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → 𝑓𝑍)
74 fdm 6013 . . . . . . . . . . . . . . . . . . . 20 (𝐹:𝑍𝑋 → dom 𝐹 = 𝑍)
7569, 74syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → dom 𝐹 = 𝑍)
7673, 75sseqtr4d 3626 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝐿) → 𝑓 ⊆ dom 𝐹)
77 funimass4 6209 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐹𝑓 ⊆ dom 𝐹) → ((𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
7871, 76, 77syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓𝐿) → ((𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
7978rexbidva 3043 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ↔ ∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
80 txflf.g . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:𝑍𝑌)
8180adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → 𝐺:𝑍𝑌)
82 ffun 6010 . . . . . . . . . . . . . . . . . . 19 (𝐺:𝑍𝑌 → Fun 𝐺)
8381, 82syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔𝐿) → Fun 𝐺)
84 filelss 21575 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑔𝐿) → 𝑔𝑍)
8524, 84sylan 488 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → 𝑔𝑍)
86 fdm 6013 . . . . . . . . . . . . . . . . . . . 20 (𝐺:𝑍𝑌 → dom 𝐺 = 𝑍)
8781, 86syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → dom 𝐺 = 𝑍)
8885, 87sseqtr4d 3626 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔𝐿) → 𝑔 ⊆ dom 𝐺)
89 funimass4 6209 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐺𝑔 ⊆ dom 𝐺) → ((𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
9083, 88, 89syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐿) → ((𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
9190rexbidva 3043 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣 ↔ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
9279, 91anbi12d 746 . . . . . . . . . . . . . . 15 (𝜑 → ((∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)))
9343, 67, 923bitr4d 300 . . . . . . . . . . . . . 14 (𝜑 → (∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣) ↔ (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
9415, 93imbi12d 334 . . . . . . . . . . . . 13 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ((𝑆𝑣𝑅𝑢) → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
95 impexp 462 . . . . . . . . . . . . 13 (((𝑆𝑣𝑅𝑢) → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
9694, 95syl6bb 276 . . . . . . . . . . . 12 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
9796ralbidv 2981 . . . . . . . . . . 11 (𝜑 → (∀𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
98 eleq2 2687 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑆𝑥𝑆𝑣))
9998ralrab 3354 . . . . . . . . . . . 12 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ ∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
100 r19.21v 2955 . . . . . . . . . . . 12 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
10199, 100bitr3i 266 . . . . . . . . . . 11 (∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
10297, 101syl6bb 276 . . . . . . . . . 10 (𝜑 → (∀𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
103102ralbidv 2981 . . . . . . . . 9 (𝜑 → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢𝐽 (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
104 eleq2 2687 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝑅𝑥𝑅𝑢))
105104ralrab 3354 . . . . . . . . 9 (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ ∀𝑢𝐽 (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
106103, 105syl6bbr 278 . . . . . . . 8 (𝜑 → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
107106adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
108 txflf.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
109 toponmax 20648 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
110108, 109syl 17 . . . . . . . . . 10 (𝜑𝑋𝐽)
111 eleq2 2687 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑅𝑥𝑅𝑋))
112111rspcev 3298 . . . . . . . . . . 11 ((𝑋𝐽𝑅𝑋) → ∃𝑥𝐽 𝑅𝑥)
113 rabn0 3937 . . . . . . . . . . 11 ({𝑥𝐽𝑅𝑥} ≠ ∅ ↔ ∃𝑥𝐽 𝑅𝑥)
114112, 113sylibr 224 . . . . . . . . . 10 ((𝑋𝐽𝑅𝑋) → {𝑥𝐽𝑅𝑥} ≠ ∅)
115110, 114sylan 488 . . . . . . . . 9 ((𝜑𝑅𝑋) → {𝑥𝐽𝑅𝑥} ≠ ∅)
116 txflf.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
117 toponmax 20648 . . . . . . . . . . 11 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
118116, 117syl 17 . . . . . . . . . 10 (𝜑𝑌𝐾)
119 eleq2 2687 . . . . . . . . . . . 12 (𝑥 = 𝑌 → (𝑆𝑥𝑆𝑌))
120119rspcev 3298 . . . . . . . . . . 11 ((𝑌𝐾𝑆𝑌) → ∃𝑥𝐾 𝑆𝑥)
121 rabn0 3937 . . . . . . . . . . 11 ({𝑥𝐾𝑆𝑥} ≠ ∅ ↔ ∃𝑥𝐾 𝑆𝑥)
122120, 121sylibr 224 . . . . . . . . . 10 ((𝑌𝐾𝑆𝑌) → {𝑥𝐾𝑆𝑥} ≠ ∅)
123118, 122sylan 488 . . . . . . . . 9 ((𝜑𝑆𝑌) → {𝑥𝐾𝑆𝑥} ≠ ∅)
124115, 123anim12dan 881 . . . . . . . 8 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → ({𝑥𝐽𝑅𝑥} ≠ ∅ ∧ {𝑥𝐾𝑆𝑥} ≠ ∅))
125 r19.28zv 4043 . . . . . . . . . 10 ({𝑥𝐾𝑆𝑥} ≠ ∅ → (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
126125ralbidv 2981 . . . . . . . . 9 ({𝑥𝐾𝑆𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
127 r19.27zv 4048 . . . . . . . . 9 ({𝑥𝐽𝑅𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
128126, 127sylan9bbr 736 . . . . . . . 8 (({𝑥𝐽𝑅𝑥} ≠ ∅ ∧ {𝑥𝐾𝑆𝑥} ≠ ∅) → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
129124, 128syl 17 . . . . . . 7 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
130107, 129bitrd 268 . . . . . 6 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
131104ralrab 3354 . . . . . . 7 (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))
13298ralrab 3354 . . . . . . 7 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))
133131, 132anbi12i 732 . . . . . 6 ((∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
134130, 133syl6bb 276 . . . . 5 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
13511, 134syl5bb 272 . . . 4 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
136135pm5.32da 672 . . 3 (𝜑 → (((𝑅𝑋𝑆𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
137 opelxp 5111 . . . 4 (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ↔ (𝑅𝑋𝑆𝑌))
138137anbi1i 730 . . 3 ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋𝑆𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)))
139 an4 864 . . 3 (((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
140136, 138, 1393bitr4g 303 . 2 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
141 eqid 2621 . . . . . . . 8 ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
142141txval 21286 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
143108, 116, 142syl2anc 692 . . . . . 6 (𝜑 → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
144143oveq1d 6625 . . . . 5 (𝜑 → ((𝐽 ×t 𝐾) fLimf 𝐿) = ((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿))
145144fveq1d 6155 . . . 4 (𝜑 → (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) = (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻))
146145eleq2d 2684 . . 3 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ ⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻)))
147 txtopon 21313 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
148108, 116, 147syl2anc 692 . . . . 5 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
149143, 148eqeltrrd 2699 . . . 4 (𝜑 → (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)))
15068ffvelrnda 6320 . . . . . 6 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ 𝑋)
15180ffvelrnda 6320 . . . . . 6 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ 𝑌)
152 opelxpi 5113 . . . . . 6 (((𝐹𝑛) ∈ 𝑋 ∧ (𝐺𝑛) ∈ 𝑌) → ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑋 × 𝑌))
153150, 151, 152syl2anc 692 . . . . 5 ((𝜑𝑛𝑍) → ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑋 × 𝑌))
154153, 47fmptd 6346 . . . 4 (𝜑𝐻:𝑍⟶(𝑋 × 𝑌))
155 eqid 2621 . . . . 5 (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)))
156155flftg 21719 . . . 4 (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐻:𝑍⟶(𝑋 × 𝑌)) → (⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
157149, 24, 154, 156syl3anc 1323 . . 3 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
158146, 157bitrd 268 . 2 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
159 isflf 21716 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐹:𝑍𝑋) → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))))
160108, 24, 68, 159syl3anc 1323 . . 3 (𝜑 → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))))
161 isflf 21716 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐺:𝑍𝑌) → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
162116, 24, 80, 161syl3anc 1323 . . 3 (𝜑 → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
163160, 162anbi12d 746 . 2 (𝜑 → ((𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)) ↔ ((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
164140, 158, 1633bitr4d 300 1 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  cin 3558  wss 3559  c0 3896  cop 4159  cmpt 4678   × cxp 5077  dom cdm 5079  ran crn 5080  cres 5081  cima 5082  Fun wfun 5846   Fn wfn 5847  wf 5848  cfv 5852  (class class class)co 6610  cmpt2 6612  topGenctg 16026  TopOnctopon 20643   ×t ctx 21282  Filcfil 21568   fLimf cflf 21658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-1st 7120  df-2nd 7121  df-map 7811  df-topgen 16032  df-fbas 19671  df-fg 19672  df-top 20627  df-topon 20644  df-bases 20670  df-ntr 20743  df-nei 20821  df-tx 21284  df-fil 21569  df-fm 21661  df-flim 21662  df-flf 21663
This theorem is referenced by:  flfcnp2  21730
  Copyright terms: Public domain W3C validator