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

Theorem txflf 23357
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 3449 . . . . . . . 8 𝑢 ∈ V
2 vex 3449 . . . . . . . 8 𝑣 ∈ V
31, 2xpex 7687 . . . . . . 7 (𝑢 × 𝑣) ∈ V
43rgen2w 3069 . . . . . 6 𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V
5 eqid 2736 . . . . . . 7 (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
6 eleq2 2826 . . . . . . . 8 (𝑧 = (𝑢 × 𝑣) → (⟨𝑅, 𝑆⟩ ∈ 𝑧 ↔ ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣)))
7 sseq2 3970 . . . . . . . . 9 (𝑧 = (𝑢 × 𝑣) → ((𝐻) ⊆ 𝑧 ↔ (𝐻) ⊆ (𝑢 × 𝑣)))
87rexbidv 3175 . . . . . . . 8 (𝑧 = (𝑢 × 𝑣) → (∃𝐿 (𝐻) ⊆ 𝑧 ↔ ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)))
96, 8imbi12d 344 . . . . . . 7 (𝑧 = (𝑢 × 𝑣) → ((⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣))))
105, 9ralrnmpo 7494 . . . . . 6 (∀𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V → (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ ∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣))))
114, 10ax-mp 5 . . . . 5 (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ ∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)))
12 opelxp 5669 . . . . . . . . . . . . . . . 16 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑅𝑢𝑆𝑣))
1312biancomi 463 . . . . . . . . . . . . . . 15 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑆𝑣𝑅𝑢))
1413a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑆𝑣𝑅𝑢)))
15 r19.40 3122 . . . . . . . . . . . . . . . . 17 (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) → (∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣))
16 raleq 3309 . . . . . . . . . . . . . . . . . . 19 ( = 𝑓 → (∀𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
1716cbvrexvw 3226 . . . . . . . . . . . . . . . . . 18 (∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢)
18 raleq 3309 . . . . . . . . . . . . . . . . . . 19 ( = 𝑔 → (∀𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
1918cbvrexvw 3226 . . . . . . . . . . . . . . . . . 18 (∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)
2017, 19anbi12i 627 . . . . . . . . . . . . . . . . 17 ((∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
2115, 20sylib 217 . . . . . . . . . . . . . . . 16 (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) → (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
22 reeanv 3217 . . . . . . . . . . . . . . . . 17 (∃𝑓𝐿𝑔𝐿 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
23 txflf.l . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐿 ∈ (Fil‘𝑍))
24 filin 23205 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓𝐿𝑔𝐿) → (𝑓𝑔) ∈ 𝐿)
25243expb 1120 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ (Fil‘𝑍) ∧ (𝑓𝐿𝑔𝐿)) → (𝑓𝑔) ∈ 𝐿)
2623, 25sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓𝐿𝑔𝐿)) → (𝑓𝑔) ∈ 𝐿)
27 inss1 4188 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑔) ⊆ 𝑓
28 ssralv 4010 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑔) ⊆ 𝑓 → (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢))
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢)
30 inss2 4189 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑔) ⊆ 𝑔
31 ssralv 4010 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑔) ⊆ 𝑔 → (∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
3230, 31ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)
3329, 32anim12i 613 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
34 raleq 3309 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑓𝑔) → (∀𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢))
35 raleq 3309 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑓𝑔) → (∀𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
3634, 35anbi12d 631 . . . . . . . . . . . . . . . . . . . . 21 ( = (𝑓𝑔) → ((∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)))
3736rspcev 3581 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝑔) ∈ 𝐿 ∧ (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
3826, 33, 37syl2an 596 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓𝐿𝑔𝐿)) ∧ (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣)) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
3938ex 413 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑓𝐿𝑔𝐿)) → ((∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4039rexlimdvva 3205 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑓𝐿𝑔𝐿 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4122, 40biimtrrid 242 . . . . . . . . . . . . . . . 16 (𝜑 → ((∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4221, 41impbid2 225 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)))
43 df-ima 5646 . . . . . . . . . . . . . . . . . . 19 (𝐻) = ran (𝐻)
44 filelss 23203 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝐿) → 𝑍)
4523, 44sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐿) → 𝑍)
46 txflf.h . . . . . . . . . . . . . . . . . . . . . . 23 𝐻 = (𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
4746reseq1i 5933 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻) = ((𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ↾ )
48 resmpt 5991 . . . . . . . . . . . . . . . . . . . . . 22 (𝑍 → ((𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ↾ ) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
4947, 48eqtrid 2788 . . . . . . . . . . . . . . . . . . . . 21 (𝑍 → (𝐻) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5045, 49syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐿) → (𝐻) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5150rneqd 5893 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐿) → ran (𝐻) = ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5243, 51eqtrid 2788 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐿) → (𝐻) = ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5352sseq1d 3975 . . . . . . . . . . . . . . . . 17 ((𝜑𝐿) → ((𝐻) ⊆ (𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣)))
54 opelxp 5669 . . . . . . . . . . . . . . . . . . 19 (⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣))
5554ralbii 3096 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ∀𝑛 ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣))
56 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
5756fmpt 7058 . . . . . . . . . . . . . . . . . . 19 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣))
58 opex 5421 . . . . . . . . . . . . . . . . . . . . 21 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ V
5958, 56fnmpti 6644 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) Fn
60 df-f 6500 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣) ↔ ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) Fn ∧ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣)))
6159, 60mpbiran 707 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣))
6257, 61bitri 274 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣))
63 r19.26 3114 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
6455, 62, 633bitr3i 300 . . . . . . . . . . . . . . . . 17 (ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
6553, 64bitrdi 286 . . . . . . . . . . . . . . . 16 ((𝜑𝐿) → ((𝐻) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
6665rexbidva 3173 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣) ↔ ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
67 txflf.f . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹:𝑍𝑋)
6867adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → 𝐹:𝑍𝑋)
6968ffund 6672 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝐿) → Fun 𝐹)
70 filelss 23203 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓𝐿) → 𝑓𝑍)
7123, 70sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → 𝑓𝑍)
7268fdmd 6679 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → dom 𝐹 = 𝑍)
7371, 72sseqtrrd 3985 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝐿) → 𝑓 ⊆ dom 𝐹)
74 funimass4 6907 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐹𝑓 ⊆ dom 𝐹) → ((𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
7569, 73, 74syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓𝐿) → ((𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
7675rexbidva 3173 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ↔ ∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
77 txflf.g . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:𝑍𝑌)
7877adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → 𝐺:𝑍𝑌)
7978ffund 6672 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔𝐿) → Fun 𝐺)
80 filelss 23203 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑔𝐿) → 𝑔𝑍)
8123, 80sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → 𝑔𝑍)
8278fdmd 6679 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → dom 𝐺 = 𝑍)
8381, 82sseqtrrd 3985 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔𝐿) → 𝑔 ⊆ dom 𝐺)
84 funimass4 6907 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐺𝑔 ⊆ dom 𝐺) → ((𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
8579, 83, 84syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐿) → ((𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
8685rexbidva 3173 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣 ↔ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
8776, 86anbi12d 631 . . . . . . . . . . . . . . 15 (𝜑 → ((∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)))
8842, 66, 873bitr4d 310 . . . . . . . . . . . . . 14 (𝜑 → (∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣) ↔ (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
8914, 88imbi12d 344 . . . . . . . . . . . . 13 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ((𝑆𝑣𝑅𝑢) → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
90 impexp 451 . . . . . . . . . . . . 13 (((𝑆𝑣𝑅𝑢) → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
9189, 90bitrdi 286 . . . . . . . . . . . 12 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
9291ralbidv 3174 . . . . . . . . . . 11 (𝜑 → (∀𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
93 eleq2 2826 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑆𝑥𝑆𝑣))
9493ralrab 3651 . . . . . . . . . . . 12 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ ∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
95 r19.21v 3176 . . . . . . . . . . . 12 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
9694, 95bitr3i 276 . . . . . . . . . . 11 (∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
9792, 96bitrdi 286 . . . . . . . . . 10 (𝜑 → (∀𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
9897ralbidv 3174 . . . . . . . . 9 (𝜑 → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢𝐽 (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
99 eleq2 2826 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝑅𝑥𝑅𝑢))
10099ralrab 3651 . . . . . . . . 9 (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ ∀𝑢𝐽 (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
10198, 100bitr4di 288 . . . . . . . 8 (𝜑 → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
102101adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
103 txflf.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
104 toponmax 22275 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
105103, 104syl 17 . . . . . . . . . 10 (𝜑𝑋𝐽)
106 eleq2 2826 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑅𝑥𝑅𝑋))
107106rspcev 3581 . . . . . . . . . . 11 ((𝑋𝐽𝑅𝑋) → ∃𝑥𝐽 𝑅𝑥)
108 rabn0 4345 . . . . . . . . . . 11 ({𝑥𝐽𝑅𝑥} ≠ ∅ ↔ ∃𝑥𝐽 𝑅𝑥)
109107, 108sylibr 233 . . . . . . . . . 10 ((𝑋𝐽𝑅𝑋) → {𝑥𝐽𝑅𝑥} ≠ ∅)
110105, 109sylan 580 . . . . . . . . 9 ((𝜑𝑅𝑋) → {𝑥𝐽𝑅𝑥} ≠ ∅)
111 txflf.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
112 toponmax 22275 . . . . . . . . . . 11 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
113111, 112syl 17 . . . . . . . . . 10 (𝜑𝑌𝐾)
114 eleq2 2826 . . . . . . . . . . . 12 (𝑥 = 𝑌 → (𝑆𝑥𝑆𝑌))
115114rspcev 3581 . . . . . . . . . . 11 ((𝑌𝐾𝑆𝑌) → ∃𝑥𝐾 𝑆𝑥)
116 rabn0 4345 . . . . . . . . . . 11 ({𝑥𝐾𝑆𝑥} ≠ ∅ ↔ ∃𝑥𝐾 𝑆𝑥)
117115, 116sylibr 233 . . . . . . . . . 10 ((𝑌𝐾𝑆𝑌) → {𝑥𝐾𝑆𝑥} ≠ ∅)
118113, 117sylan 580 . . . . . . . . 9 ((𝜑𝑆𝑌) → {𝑥𝐾𝑆𝑥} ≠ ∅)
119110, 118anim12dan 619 . . . . . . . 8 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → ({𝑥𝐽𝑅𝑥} ≠ ∅ ∧ {𝑥𝐾𝑆𝑥} ≠ ∅))
120 r19.28zv 4458 . . . . . . . . . 10 ({𝑥𝐾𝑆𝑥} ≠ ∅ → (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
121120ralbidv 3174 . . . . . . . . 9 ({𝑥𝐾𝑆𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
122 r19.27zv 4463 . . . . . . . . 9 ({𝑥𝐽𝑅𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
123121, 122sylan9bbr 511 . . . . . . . 8 (({𝑥𝐽𝑅𝑥} ≠ ∅ ∧ {𝑥𝐾𝑆𝑥} ≠ ∅) → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
124119, 123syl 17 . . . . . . 7 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
125102, 124bitrd 278 . . . . . 6 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
12699ralrab 3651 . . . . . . 7 (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))
12793ralrab 3651 . . . . . . 7 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))
128126, 127anbi12i 627 . . . . . 6 ((∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
129125, 128bitrdi 286 . . . . 5 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
13011, 129bitrid 282 . . . 4 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
131130pm5.32da 579 . . 3 (𝜑 → (((𝑅𝑋𝑆𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
132 opelxp 5669 . . . 4 (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ↔ (𝑅𝑋𝑆𝑌))
133132anbi1i 624 . . 3 ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋𝑆𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)))
134 an4 654 . . 3 (((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
135131, 133, 1343bitr4g 313 . 2 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
136 eqid 2736 . . . . . . . 8 ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
137136txval 22915 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
138103, 111, 137syl2anc 584 . . . . . 6 (𝜑 → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
139138oveq1d 7372 . . . . 5 (𝜑 → ((𝐽 ×t 𝐾) fLimf 𝐿) = ((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿))
140139fveq1d 6844 . . . 4 (𝜑 → (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) = (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻))
141140eleq2d 2823 . . 3 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ ⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻)))
142 txtopon 22942 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
143103, 111, 142syl2anc 584 . . . . 5 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
144138, 143eqeltrrd 2839 . . . 4 (𝜑 → (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)))
14567ffvelcdmda 7035 . . . . . 6 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ 𝑋)
14677ffvelcdmda 7035 . . . . . 6 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ 𝑌)
147145, 146opelxpd 5671 . . . . 5 ((𝜑𝑛𝑍) → ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑋 × 𝑌))
148147, 46fmptd 7062 . . . 4 (𝜑𝐻:𝑍⟶(𝑋 × 𝑌))
149 eqid 2736 . . . . 5 (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)))
150149flftg 23347 . . . 4 (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐻:𝑍⟶(𝑋 × 𝑌)) → (⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
151144, 23, 148, 150syl3anc 1371 . . 3 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
152141, 151bitrd 278 . 2 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
153 isflf 23344 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐹:𝑍𝑋) → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))))
154103, 23, 67, 153syl3anc 1371 . . 3 (𝜑 → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))))
155 isflf 23344 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐺:𝑍𝑌) → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
156111, 23, 77, 155syl3anc 1371 . . 3 (𝜑 → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
157154, 156anbi12d 631 . 2 (𝜑 → ((𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)) ↔ ((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
158135, 152, 1573bitr4d 310 1 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cin 3909  wss 3910  c0 4282  cop 4592  cmpt 5188   × cxp 5631  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  Fun wfun 6490   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  topGenctg 17319  TopOnctopon 22259   ×t ctx 22911  Filcfil 23196   fLimf cflf 23286
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-rep 5242  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-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  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-f1 6501  df-fo 6502  df-f1o 6503  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-fbas 20793  df-fg 20794  df-top 22243  df-topon 22260  df-bases 22296  df-ntr 22371  df-nei 22449  df-tx 22913  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291
This theorem is referenced by:  flfcnp2  23358
  Copyright terms: Public domain W3C validator