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

Theorem txflf 23492
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 3479 . . . . . . . 8 𝑢 ∈ V
2 vex 3479 . . . . . . . 8 𝑣 ∈ V
31, 2xpex 7735 . . . . . . 7 (𝑢 × 𝑣) ∈ V
43rgen2w 3067 . . . . . 6 𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V
5 eqid 2733 . . . . . . 7 (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
6 eleq2 2823 . . . . . . . 8 (𝑧 = (𝑢 × 𝑣) → (⟨𝑅, 𝑆⟩ ∈ 𝑧 ↔ ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣)))
7 sseq2 4007 . . . . . . . . 9 (𝑧 = (𝑢 × 𝑣) → ((𝐻) ⊆ 𝑧 ↔ (𝐻) ⊆ (𝑢 × 𝑣)))
87rexbidv 3179 . . . . . . . 8 (𝑧 = (𝑢 × 𝑣) → (∃𝐿 (𝐻) ⊆ 𝑧 ↔ ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)))
96, 8imbi12d 345 . . . . . . 7 (𝑧 = (𝑢 × 𝑣) → ((⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣))))
105, 9ralrnmpo 7542 . . . . . 6 (∀𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V → (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ ∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣))))
114, 10ax-mp 5 . . . . 5 (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ ∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)))
12 opelxp 5711 . . . . . . . . . . . . . . . 16 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑅𝑢𝑆𝑣))
1312biancomi 464 . . . . . . . . . . . . . . 15 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑆𝑣𝑅𝑢))
1413a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑆𝑣𝑅𝑢)))
15 r19.40 3120 . . . . . . . . . . . . . . . . 17 (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) → (∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣))
16 raleq 3323 . . . . . . . . . . . . . . . . . . 19 ( = 𝑓 → (∀𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
1716cbvrexvw 3236 . . . . . . . . . . . . . . . . . 18 (∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢)
18 raleq 3323 . . . . . . . . . . . . . . . . . . 19 ( = 𝑔 → (∀𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
1918cbvrexvw 3236 . . . . . . . . . . . . . . . . . 18 (∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)
2017, 19anbi12i 628 . . . . . . . . . . . . . . . . 17 ((∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
2115, 20sylib 217 . . . . . . . . . . . . . . . 16 (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) → (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
22 reeanv 3227 . . . . . . . . . . . . . . . . 17 (∃𝑓𝐿𝑔𝐿 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
23 txflf.l . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐿 ∈ (Fil‘𝑍))
24 filin 23340 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓𝐿𝑔𝐿) → (𝑓𝑔) ∈ 𝐿)
25243expb 1121 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ (Fil‘𝑍) ∧ (𝑓𝐿𝑔𝐿)) → (𝑓𝑔) ∈ 𝐿)
2623, 25sylan 581 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓𝐿𝑔𝐿)) → (𝑓𝑔) ∈ 𝐿)
27 inss1 4227 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑔) ⊆ 𝑓
28 ssralv 4049 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑔) ⊆ 𝑓 → (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢))
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢)
30 inss2 4228 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑔) ⊆ 𝑔
31 ssralv 4049 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑔) ⊆ 𝑔 → (∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
3230, 31ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)
3329, 32anim12i 614 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
34 raleq 3323 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑓𝑔) → (∀𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢))
35 raleq 3323 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑓𝑔) → (∀𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
3634, 35anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 ( = (𝑓𝑔) → ((∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)))
3736rspcev 3612 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝑔) ∈ 𝐿 ∧ (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
3826, 33, 37syl2an 597 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓𝐿𝑔𝐿)) ∧ (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣)) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
3938ex 414 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑓𝐿𝑔𝐿)) → ((∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4039rexlimdvva 3212 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑓𝐿𝑔𝐿 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4122, 40biimtrrid 242 . . . . . . . . . . . . . . . 16 (𝜑 → ((∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4221, 41impbid2 225 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)))
43 df-ima 5688 . . . . . . . . . . . . . . . . . . 19 (𝐻) = ran (𝐻)
44 filelss 23338 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝐿) → 𝑍)
4523, 44sylan 581 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐿) → 𝑍)
46 txflf.h . . . . . . . . . . . . . . . . . . . . . . 23 𝐻 = (𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
4746reseq1i 5975 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻) = ((𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ↾ )
48 resmpt 6035 . . . . . . . . . . . . . . . . . . . . . 22 (𝑍 → ((𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ↾ ) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
4947, 48eqtrid 2785 . . . . . . . . . . . . . . . . . . . . 21 (𝑍 → (𝐻) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5045, 49syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐿) → (𝐻) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5150rneqd 5935 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐿) → ran (𝐻) = ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5243, 51eqtrid 2785 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐿) → (𝐻) = ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5352sseq1d 4012 . . . . . . . . . . . . . . . . 17 ((𝜑𝐿) → ((𝐻) ⊆ (𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣)))
54 opelxp 5711 . . . . . . . . . . . . . . . . . . 19 (⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣))
5554ralbii 3094 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ∀𝑛 ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣))
56 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
5756fmpt 7105 . . . . . . . . . . . . . . . . . . 19 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣))
58 opex 5463 . . . . . . . . . . . . . . . . . . . . 21 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ V
5958, 56fnmpti 6690 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) Fn
60 df-f 6544 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣) ↔ ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) Fn ∧ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣)))
6159, 60mpbiran 708 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣))
6257, 61bitri 275 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣))
63 r19.26 3112 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
6455, 62, 633bitr3i 301 . . . . . . . . . . . . . . . . 17 (ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
6553, 64bitrdi 287 . . . . . . . . . . . . . . . 16 ((𝜑𝐿) → ((𝐻) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
6665rexbidva 3177 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣) ↔ ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
67 txflf.f . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹:𝑍𝑋)
6867adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → 𝐹:𝑍𝑋)
6968ffund 6718 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝐿) → Fun 𝐹)
70 filelss 23338 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓𝐿) → 𝑓𝑍)
7123, 70sylan 581 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → 𝑓𝑍)
7268fdmd 6725 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → dom 𝐹 = 𝑍)
7371, 72sseqtrrd 4022 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝐿) → 𝑓 ⊆ dom 𝐹)
74 funimass4 6953 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐹𝑓 ⊆ dom 𝐹) → ((𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
7569, 73, 74syl2anc 585 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓𝐿) → ((𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
7675rexbidva 3177 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ↔ ∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
77 txflf.g . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:𝑍𝑌)
7877adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → 𝐺:𝑍𝑌)
7978ffund 6718 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔𝐿) → Fun 𝐺)
80 filelss 23338 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑔𝐿) → 𝑔𝑍)
8123, 80sylan 581 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → 𝑔𝑍)
8278fdmd 6725 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → dom 𝐺 = 𝑍)
8381, 82sseqtrrd 4022 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔𝐿) → 𝑔 ⊆ dom 𝐺)
84 funimass4 6953 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐺𝑔 ⊆ dom 𝐺) → ((𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
8579, 83, 84syl2anc 585 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐿) → ((𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
8685rexbidva 3177 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣 ↔ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
8776, 86anbi12d 632 . . . . . . . . . . . . . . 15 (𝜑 → ((∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)))
8842, 66, 873bitr4d 311 . . . . . . . . . . . . . 14 (𝜑 → (∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣) ↔ (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
8914, 88imbi12d 345 . . . . . . . . . . . . 13 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ((𝑆𝑣𝑅𝑢) → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
90 impexp 452 . . . . . . . . . . . . 13 (((𝑆𝑣𝑅𝑢) → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
9189, 90bitrdi 287 . . . . . . . . . . . 12 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
9291ralbidv 3178 . . . . . . . . . . 11 (𝜑 → (∀𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
93 eleq2 2823 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑆𝑥𝑆𝑣))
9493ralrab 3688 . . . . . . . . . . . 12 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ ∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
95 r19.21v 3180 . . . . . . . . . . . 12 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
9694, 95bitr3i 277 . . . . . . . . . . 11 (∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
9792, 96bitrdi 287 . . . . . . . . . 10 (𝜑 → (∀𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
9897ralbidv 3178 . . . . . . . . 9 (𝜑 → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢𝐽 (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
99 eleq2 2823 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝑅𝑥𝑅𝑢))
10099ralrab 3688 . . . . . . . . 9 (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ ∀𝑢𝐽 (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
10198, 100bitr4di 289 . . . . . . . 8 (𝜑 → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
102101adantr 482 . . . . . . 7 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
103 txflf.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
104 toponmax 22410 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
105103, 104syl 17 . . . . . . . . . 10 (𝜑𝑋𝐽)
106 eleq2 2823 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑅𝑥𝑅𝑋))
107106rspcev 3612 . . . . . . . . . . 11 ((𝑋𝐽𝑅𝑋) → ∃𝑥𝐽 𝑅𝑥)
108 rabn0 4384 . . . . . . . . . . 11 ({𝑥𝐽𝑅𝑥} ≠ ∅ ↔ ∃𝑥𝐽 𝑅𝑥)
109107, 108sylibr 233 . . . . . . . . . 10 ((𝑋𝐽𝑅𝑋) → {𝑥𝐽𝑅𝑥} ≠ ∅)
110105, 109sylan 581 . . . . . . . . 9 ((𝜑𝑅𝑋) → {𝑥𝐽𝑅𝑥} ≠ ∅)
111 txflf.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
112 toponmax 22410 . . . . . . . . . . 11 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
113111, 112syl 17 . . . . . . . . . 10 (𝜑𝑌𝐾)
114 eleq2 2823 . . . . . . . . . . . 12 (𝑥 = 𝑌 → (𝑆𝑥𝑆𝑌))
115114rspcev 3612 . . . . . . . . . . 11 ((𝑌𝐾𝑆𝑌) → ∃𝑥𝐾 𝑆𝑥)
116 rabn0 4384 . . . . . . . . . . 11 ({𝑥𝐾𝑆𝑥} ≠ ∅ ↔ ∃𝑥𝐾 𝑆𝑥)
117115, 116sylibr 233 . . . . . . . . . 10 ((𝑌𝐾𝑆𝑌) → {𝑥𝐾𝑆𝑥} ≠ ∅)
118113, 117sylan 581 . . . . . . . . 9 ((𝜑𝑆𝑌) → {𝑥𝐾𝑆𝑥} ≠ ∅)
119110, 118anim12dan 620 . . . . . . . 8 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → ({𝑥𝐽𝑅𝑥} ≠ ∅ ∧ {𝑥𝐾𝑆𝑥} ≠ ∅))
120 r19.28zv 4499 . . . . . . . . . 10 ({𝑥𝐾𝑆𝑥} ≠ ∅ → (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
121120ralbidv 3178 . . . . . . . . 9 ({𝑥𝐾𝑆𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
122 r19.27zv 4504 . . . . . . . . 9 ({𝑥𝐽𝑅𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
123121, 122sylan9bbr 512 . . . . . . . 8 (({𝑥𝐽𝑅𝑥} ≠ ∅ ∧ {𝑥𝐾𝑆𝑥} ≠ ∅) → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
124119, 123syl 17 . . . . . . 7 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
125102, 124bitrd 279 . . . . . 6 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
12699ralrab 3688 . . . . . . 7 (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))
12793ralrab 3688 . . . . . . 7 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))
128126, 127anbi12i 628 . . . . . 6 ((∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
129125, 128bitrdi 287 . . . . 5 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
13011, 129bitrid 283 . . . 4 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
131130pm5.32da 580 . . 3 (𝜑 → (((𝑅𝑋𝑆𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
132 opelxp 5711 . . . 4 (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ↔ (𝑅𝑋𝑆𝑌))
133132anbi1i 625 . . 3 ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋𝑆𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)))
134 an4 655 . . 3 (((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
135131, 133, 1343bitr4g 314 . 2 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
136 eqid 2733 . . . . . . . 8 ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
137136txval 23050 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
138103, 111, 137syl2anc 585 . . . . . 6 (𝜑 → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
139138oveq1d 7419 . . . . 5 (𝜑 → ((𝐽 ×t 𝐾) fLimf 𝐿) = ((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿))
140139fveq1d 6890 . . . 4 (𝜑 → (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) = (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻))
141140eleq2d 2820 . . 3 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ ⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻)))
142 txtopon 23077 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
143103, 111, 142syl2anc 585 . . . . 5 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
144138, 143eqeltrrd 2835 . . . 4 (𝜑 → (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)))
14567ffvelcdmda 7082 . . . . . 6 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ 𝑋)
14677ffvelcdmda 7082 . . . . . 6 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ 𝑌)
147145, 146opelxpd 5713 . . . . 5 ((𝜑𝑛𝑍) → ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑋 × 𝑌))
148147, 46fmptd 7109 . . . 4 (𝜑𝐻:𝑍⟶(𝑋 × 𝑌))
149 eqid 2733 . . . . 5 (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)))
150149flftg 23482 . . . 4 (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐻:𝑍⟶(𝑋 × 𝑌)) → (⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
151144, 23, 148, 150syl3anc 1372 . . 3 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
152141, 151bitrd 279 . 2 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
153 isflf 23479 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐹:𝑍𝑋) → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))))
154103, 23, 67, 153syl3anc 1372 . . 3 (𝜑 → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))))
155 isflf 23479 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐺:𝑍𝑌) → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
156111, 23, 77, 155syl3anc 1372 . . 3 (𝜑 → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
157154, 156anbi12d 632 . 2 (𝜑 → ((𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)) ↔ ((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
158135, 152, 1573bitr4d 311 1 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wne 2941  wral 3062  wrex 3071  {crab 3433  Vcvv 3475  cin 3946  wss 3947  c0 4321  cop 4633  cmpt 5230   × cxp 5673  dom cdm 5675  ran crn 5676  cres 5677  cima 5678  Fun wfun 6534   Fn wfn 6535  wf 6536  cfv 6540  (class class class)co 7404  cmpo 7406  topGenctg 17379  TopOnctopon 22394   ×t ctx 23046  Filcfil 23331   fLimf cflf 23421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7970  df-2nd 7971  df-map 8818  df-topgen 17385  df-fbas 20926  df-fg 20927  df-top 22378  df-topon 22395  df-bases 22431  df-ntr 22506  df-nei 22584  df-tx 23048  df-fil 23332  df-fm 23424  df-flim 23425  df-flf 23426
This theorem is referenced by:  flfcnp2  23493
  Copyright terms: Public domain W3C validator