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

Theorem txflf 22617
 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 3500 . . . . . . . 8 𝑢 ∈ V
2 vex 3500 . . . . . . . 8 𝑣 ∈ V
31, 2xpex 7479 . . . . . . 7 (𝑢 × 𝑣) ∈ V
43rgen2w 3154 . . . . . 6 𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V
5 eqid 2824 . . . . . . 7 (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
6 eleq2 2904 . . . . . . . 8 (𝑧 = (𝑢 × 𝑣) → (⟨𝑅, 𝑆⟩ ∈ 𝑧 ↔ ⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣)))
7 sseq2 3996 . . . . . . . . 9 (𝑧 = (𝑢 × 𝑣) → ((𝐻) ⊆ 𝑧 ↔ (𝐻) ⊆ (𝑢 × 𝑣)))
87rexbidv 3300 . . . . . . . 8 (𝑧 = (𝑢 × 𝑣) → (∃𝐿 (𝐻) ⊆ 𝑧 ↔ ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)))
96, 8imbi12d 347 . . . . . . 7 (𝑧 = (𝑢 × 𝑣) → ((⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣))))
105, 9ralrnmpo 7292 . . . . . 6 (∀𝑢𝐽𝑣𝐾 (𝑢 × 𝑣) ∈ V → (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ ∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣))))
114, 10ax-mp 5 . . . . 5 (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ ∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)))
12 opelxp 5594 . . . . . . . . . . . . . . . 16 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑅𝑢𝑆𝑣))
1312biancomi 465 . . . . . . . . . . . . . . 15 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑆𝑣𝑅𝑢))
1413a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) ↔ (𝑆𝑣𝑅𝑢)))
15 r19.40 3349 . . . . . . . . . . . . . . . . 17 (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) → (∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣))
16 raleq 3408 . . . . . . . . . . . . . . . . . . 19 ( = 𝑓 → (∀𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
1716cbvrexvw 3453 . . . . . . . . . . . . . . . . . 18 (∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢)
18 raleq 3408 . . . . . . . . . . . . . . . . . . 19 ( = 𝑔 → (∀𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
1918cbvrexvw 3453 . . . . . . . . . . . . . . . . . 18 (∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)
2017, 19anbi12i 628 . . . . . . . . . . . . . . . . 17 ((∃𝐿𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝐿𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
2115, 20sylib 220 . . . . . . . . . . . . . . . 16 (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) → (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
22 reeanv 3370 . . . . . . . . . . . . . . . . 17 (∃𝑓𝐿𝑔𝐿 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
23 txflf.l . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐿 ∈ (Fil‘𝑍))
24 filin 22465 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓𝐿𝑔𝐿) → (𝑓𝑔) ∈ 𝐿)
25243expb 1116 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ (Fil‘𝑍) ∧ (𝑓𝐿𝑔𝐿)) → (𝑓𝑔) ∈ 𝐿)
2623, 25sylan 582 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑓𝐿𝑔𝐿)) → (𝑓𝑔) ∈ 𝐿)
27 inss1 4208 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑔) ⊆ 𝑓
28 ssralv 4036 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑔) ⊆ 𝑓 → (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢))
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢)
30 inss2 4209 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑔) ⊆ 𝑔
31 ssralv 4036 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑔) ⊆ 𝑔 → (∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
3230, 31ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)
3329, 32anim12i 614 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
34 raleq 3408 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑓𝑔) → (∀𝑛 (𝐹𝑛) ∈ 𝑢 ↔ ∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢))
35 raleq 3408 . . . . . . . . . . . . . . . . . . . . . 22 ( = (𝑓𝑔) → (∀𝑛 (𝐺𝑛) ∈ 𝑣 ↔ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣))
3634, 35anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 ( = (𝑓𝑔) → ((∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)))
3736rspcev 3626 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝑔) ∈ 𝐿 ∧ (∀𝑛 ∈ (𝑓𝑔)(𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓𝑔)(𝐺𝑛) ∈ 𝑣)) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
3826, 33, 37syl2an 597 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓𝐿𝑔𝐿)) ∧ (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣)) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
3938ex 415 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑓𝐿𝑔𝐿)) → ((∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4039rexlimdvva 3297 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑓𝐿𝑔𝐿 (∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4122, 40syl5bir 245 . . . . . . . . . . . . . . . 16 (𝜑 → ((∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣) → ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
4221, 41impbid2 228 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)))
43 df-ima 5571 . . . . . . . . . . . . . . . . . . 19 (𝐻) = ran (𝐻)
44 filelss 22463 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝐿) → 𝑍)
4523, 44sylan 582 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐿) → 𝑍)
46 txflf.h . . . . . . . . . . . . . . . . . . . . . . 23 𝐻 = (𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
4746reseq1i 5852 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻) = ((𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ↾ )
48 resmpt 5908 . . . . . . . . . . . . . . . . . . . . . 22 (𝑍 → ((𝑛𝑍 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ↾ ) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
4947, 48syl5eq 2871 . . . . . . . . . . . . . . . . . . . . 21 (𝑍 → (𝐻) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5045, 49syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐿) → (𝐻) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5150rneqd 5811 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐿) → ran (𝐻) = ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5243, 51syl5eq 2871 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐿) → (𝐻) = ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩))
5352sseq1d 4001 . . . . . . . . . . . . . . . . 17 ((𝜑𝐿) → ((𝐻) ⊆ (𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣)))
54 opelxp 5594 . . . . . . . . . . . . . . . . . . 19 (⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣))
5554ralbii 3168 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ∀𝑛 ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣))
56 eqid 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) = (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩)
5756fmpt 6877 . . . . . . . . . . . . . . . . . . 19 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣))
58 opex 5359 . . . . . . . . . . . . . . . . . . . . 21 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ V
5958, 56fnmpti 6494 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) Fn
60 df-f 6362 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣) ↔ ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) Fn ∧ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣)))
6159, 60mpbiran 707 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩):⟶(𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣))
6257, 61bitri 277 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑢 × 𝑣) ↔ ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣))
63 r19.26 3173 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ((𝐹𝑛) ∈ 𝑢 ∧ (𝐺𝑛) ∈ 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
6455, 62, 633bitr3i 303 . . . . . . . . . . . . . . . . 17 (ran (𝑛 ↦ ⟨(𝐹𝑛), (𝐺𝑛)⟩) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣))
6553, 64syl6bb 289 . . . . . . . . . . . . . . . 16 ((𝜑𝐿) → ((𝐻) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
6665rexbidva 3299 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣) ↔ ∃𝐿 (∀𝑛 (𝐹𝑛) ∈ 𝑢 ∧ ∀𝑛 (𝐺𝑛) ∈ 𝑣)))
67 txflf.f . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐹:𝑍𝑋)
6867adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → 𝐹:𝑍𝑋)
6968ffund 6521 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝐿) → Fun 𝐹)
70 filelss 22463 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓𝐿) → 𝑓𝑍)
7123, 70sylan 582 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → 𝑓𝑍)
7268fdmd 6526 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝐿) → dom 𝐹 = 𝑍)
7371, 72sseqtrrd 4011 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝐿) → 𝑓 ⊆ dom 𝐹)
74 funimass4 6733 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐹𝑓 ⊆ dom 𝐹) → ((𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
7569, 73, 74syl2anc 586 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓𝐿) → ((𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
7675rexbidva 3299 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ↔ ∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢))
77 txflf.g . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:𝑍𝑌)
7877adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → 𝐺:𝑍𝑌)
7978ffund 6521 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔𝐿) → Fun 𝐺)
80 filelss 22463 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑔𝐿) → 𝑔𝑍)
8123, 80sylan 582 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → 𝑔𝑍)
8278fdmd 6526 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑔𝐿) → dom 𝐺 = 𝑍)
8381, 82sseqtrrd 4011 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑔𝐿) → 𝑔 ⊆ dom 𝐺)
84 funimass4 6733 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐺𝑔 ⊆ dom 𝐺) → ((𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
8579, 83, 84syl2anc 586 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔𝐿) → ((𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
8685rexbidva 3299 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣 ↔ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣))
8776, 86anbi12d 632 . . . . . . . . . . . . . . 15 (𝜑 → ((∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∃𝑓𝐿𝑛𝑓 (𝐹𝑛) ∈ 𝑢 ∧ ∃𝑔𝐿𝑛𝑔 (𝐺𝑛) ∈ 𝑣)))
8842, 66, 873bitr4d 313 . . . . . . . . . . . . . 14 (𝜑 → (∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣) ↔ (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
8914, 88imbi12d 347 . . . . . . . . . . . . 13 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ((𝑆𝑣𝑅𝑢) → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
90 impexp 453 . . . . . . . . . . . . 13 (((𝑆𝑣𝑅𝑢) → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
9189, 90syl6bb 289 . . . . . . . . . . . 12 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
9291ralbidv 3200 . . . . . . . . . . 11 (𝜑 → (∀𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
93 eleq2 2904 . . . . . . . . . . . . 13 (𝑥 = 𝑣 → (𝑆𝑥𝑆𝑣))
9493ralrab 3688 . . . . . . . . . . . 12 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ ∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
95 r19.21v 3178 . . . . . . . . . . . 12 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
9694, 95bitr3i 279 . . . . . . . . . . 11 (∀𝑣𝐾 (𝑆𝑣 → (𝑅𝑢 → (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
9792, 96syl6bb 289 . . . . . . . . . 10 (𝜑 → (∀𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
9897ralbidv 3200 . . . . . . . . 9 (𝜑 → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢𝐽 (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
99 eleq2 2904 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝑅𝑥𝑅𝑢))
10099ralrab 3688 . . . . . . . . 9 (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ ∀𝑢𝐽 (𝑅𝑢 → ∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
10198, 100syl6bbr 291 . . . . . . . 8 (𝜑 → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
102101adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
103 txflf.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
104 toponmax 21537 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
105103, 104syl 17 . . . . . . . . . 10 (𝜑𝑋𝐽)
106 eleq2 2904 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑅𝑥𝑅𝑋))
107106rspcev 3626 . . . . . . . . . . 11 ((𝑋𝐽𝑅𝑋) → ∃𝑥𝐽 𝑅𝑥)
108 rabn0 4342 . . . . . . . . . . 11 ({𝑥𝐽𝑅𝑥} ≠ ∅ ↔ ∃𝑥𝐽 𝑅𝑥)
109107, 108sylibr 236 . . . . . . . . . 10 ((𝑋𝐽𝑅𝑋) → {𝑥𝐽𝑅𝑥} ≠ ∅)
110105, 109sylan 582 . . . . . . . . 9 ((𝜑𝑅𝑋) → {𝑥𝐽𝑅𝑥} ≠ ∅)
111 txflf.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
112 toponmax 21537 . . . . . . . . . . 11 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
113111, 112syl 17 . . . . . . . . . 10 (𝜑𝑌𝐾)
114 eleq2 2904 . . . . . . . . . . . 12 (𝑥 = 𝑌 → (𝑆𝑥𝑆𝑌))
115114rspcev 3626 . . . . . . . . . . 11 ((𝑌𝐾𝑆𝑌) → ∃𝑥𝐾 𝑆𝑥)
116 rabn0 4342 . . . . . . . . . . 11 ({𝑥𝐾𝑆𝑥} ≠ ∅ ↔ ∃𝑥𝐾 𝑆𝑥)
117115, 116sylibr 236 . . . . . . . . . 10 ((𝑌𝐾𝑆𝑌) → {𝑥𝐾𝑆𝑥} ≠ ∅)
118113, 117sylan 582 . . . . . . . . 9 ((𝜑𝑆𝑌) → {𝑥𝐾𝑆𝑥} ≠ ∅)
119110, 118anim12dan 620 . . . . . . . 8 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → ({𝑥𝐽𝑅𝑥} ≠ ∅ ∧ {𝑥𝐾𝑆𝑥} ≠ ∅))
120 r19.28zv 4449 . . . . . . . . . 10 ({𝑥𝐾𝑆𝑥} ≠ ∅ → (∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
121120ralbidv 3200 . . . . . . . . 9 ({𝑥𝐾𝑆𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ ∀𝑢 ∈ {𝑥𝐽𝑅𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
122 r19.27zv 4454 . . . . . . . . 9 ({𝑥𝐽𝑅𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
123121, 122sylan9bbr 513 . . . . . . . 8 (({𝑥𝐽𝑅𝑥} ≠ ∅ ∧ {𝑥𝐾𝑆𝑥} ≠ ∅) → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
124119, 123syl 17 . . . . . . 7 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∀𝑣 ∈ {𝑥𝐾𝑆𝑥} (∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
125102, 124bitrd 281 . . . . . 6 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
12699ralrab 3688 . . . . . . 7 (∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ↔ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))
12793ralrab 3688 . . . . . . 7 (∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣 ↔ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))
128126, 127anbi12i 628 . . . . . 6 ((∀𝑢 ∈ {𝑥𝐽𝑅𝑥}∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥𝐾𝑆𝑥}∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))
129125, 128syl6bb 289 . . . . 5 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑢𝐽𝑣𝐾 (⟨𝑅, 𝑆⟩ ∈ (𝑢 × 𝑣) → ∃𝐿 (𝐻) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
13011, 129syl5bb 285 . . . 4 ((𝜑 ∧ (𝑅𝑋𝑆𝑌)) → (∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧) ↔ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
131130pm5.32da 581 . . 3 (𝜑 → (((𝑅𝑋𝑆𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
132 opelxp 5594 . . . 4 (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ↔ (𝑅𝑋𝑆𝑌))
133132anbi1i 625 . . 3 ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋𝑆𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)))
134 an4 654 . . 3 (((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))) ↔ ((𝑅𝑋𝑆𝑌) ∧ (∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢) ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
135131, 133, 1343bitr4g 316 . 2 (𝜑 → ((⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧)) ↔ ((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
136 eqid 2824 . . . . . . . 8 ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)) = ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))
137136txval 22175 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
138103, 111, 137syl2anc 586 . . . . . 6 (𝜑 → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))))
139138oveq1d 7174 . . . . 5 (𝜑 → ((𝐽 ×t 𝐾) fLimf 𝐿) = ((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿))
140139fveq1d 6675 . . . 4 (𝜑 → (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) = (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻))
141140eleq2d 2901 . . 3 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ ⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻)))
142 txtopon 22202 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
143103, 111, 142syl2anc 586 . . . . 5 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
144138, 143eqeltrrd 2917 . . . 4 (𝜑 → (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)))
14567ffvelrnda 6854 . . . . . 6 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ 𝑋)
14677ffvelrnda 6854 . . . . . 6 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ 𝑌)
147145, 146opelxpd 5596 . . . . 5 ((𝜑𝑛𝑍) → ⟨(𝐹𝑛), (𝐺𝑛)⟩ ∈ (𝑋 × 𝑌))
148147, 46fmptd 6881 . . . 4 (𝜑𝐻:𝑍⟶(𝑋 × 𝑌))
149 eqid 2824 . . . . 5 (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) = (topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣)))
150149flftg 22607 . . . 4 (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐻:𝑍⟶(𝑋 × 𝑌)) → (⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
151144, 23, 148, 150syl3anc 1367 . . 3 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((topGen‘ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
152141, 151bitrd 281 . 2 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (⟨𝑅, 𝑆⟩ ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢𝐽, 𝑣𝐾 ↦ (𝑢 × 𝑣))(⟨𝑅, 𝑆⟩ ∈ 𝑧 → ∃𝐿 (𝐻) ⊆ 𝑧))))
153 isflf 22604 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐹:𝑍𝑋) → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))))
154103, 23, 67, 153syl3anc 1367 . . 3 (𝜑 → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢))))
155 isflf 22604 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐺:𝑍𝑌) → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
156111, 23, 77, 155syl3anc 1367 . . 3 (𝜑 → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣))))
157154, 156anbi12d 632 . 2 (𝜑 → ((𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)) ↔ ((𝑅𝑋 ∧ ∀𝑢𝐽 (𝑅𝑢 → ∃𝑓𝐿 (𝐹𝑓) ⊆ 𝑢)) ∧ (𝑆𝑌 ∧ ∀𝑣𝐾 (𝑆𝑣 → ∃𝑔𝐿 (𝐺𝑔) ⊆ 𝑣)))))
158135, 152, 1573bitr4d 313 1 (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536   ∈ wcel 2113   ≠ wne 3019  ∀wral 3141  ∃wrex 3142  {crab 3145  Vcvv 3497   ∩ cin 3938   ⊆ wss 3939  ∅c0 4294  ⟨cop 4576   ↦ cmpt 5149   × cxp 5556  dom cdm 5558  ran crn 5559   ↾ cres 5560   “ cima 5561  Fun wfun 6352   Fn wfn 6353  ⟶wf 6354  ‘cfv 6358  (class class class)co 7159   ∈ cmpo 7161  topGenctg 16714  TopOnctopon 21521   ×t ctx 22171  Filcfil 22456   fLimf cflf 22546 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7162  df-oprab 7163  df-mpo 7164  df-1st 7692  df-2nd 7693  df-map 8411  df-topgen 16720  df-fbas 20545  df-fg 20546  df-top 21505  df-topon 21522  df-bases 21557  df-ntr 21631  df-nei 21709  df-tx 22173  df-fil 22457  df-fm 22549  df-flim 22550  df-flf 22551 This theorem is referenced by:  flfcnp2  22618
 Copyright terms: Public domain W3C validator