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

Theorem txflf 23509
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 3478 . . . . . . . 8 𝑒 ∈ V
2 vex 3478 . . . . . . . 8 𝑣 ∈ V
31, 2xpex 7739 . . . . . . 7 (𝑒 Γ— 𝑣) ∈ V
43rgen2w 3066 . . . . . 6 βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (𝑒 Γ— 𝑣) ∈ V
5 eqid 2732 . . . . . . 7 (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣)) = (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))
6 eleq2 2822 . . . . . . . 8 (𝑧 = (𝑒 Γ— 𝑣) β†’ (βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 ↔ βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣)))
7 sseq2 4008 . . . . . . . . 9 (𝑧 = (𝑒 Γ— 𝑣) β†’ ((𝐻 β€œ β„Ž) βŠ† 𝑧 ↔ (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)))
87rexbidv 3178 . . . . . . . 8 (𝑧 = (𝑒 Γ— 𝑣) β†’ (βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧 ↔ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)))
96, 8imbi12d 344 . . . . . . 7 (𝑧 = (𝑒 Γ— 𝑣) β†’ ((βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧) ↔ (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣))))
105, 9ralrnmpo 7546 . . . . . 6 (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (𝑒 Γ— 𝑣) ∈ V β†’ (βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧) ↔ βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣))))
114, 10ax-mp 5 . . . . 5 (βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧) ↔ βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)))
12 opelxp 5712 . . . . . . . . . . . . . . . 16 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) ↔ (𝑅 ∈ 𝑒 ∧ 𝑆 ∈ 𝑣))
1312biancomi 463 . . . . . . . . . . . . . . 15 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) ↔ (𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑒))
1413a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) ↔ (𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑒)))
15 r19.40 3119 . . . . . . . . . . . . . . . . 17 (βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) β†’ (βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
16 raleq 3322 . . . . . . . . . . . . . . . . . . 19 (β„Ž = 𝑓 β†’ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ↔ βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒))
1716cbvrexvw 3235 . . . . . . . . . . . . . . . . . 18 (βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ↔ βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒)
18 raleq 3322 . . . . . . . . . . . . . . . . . . 19 (β„Ž = 𝑔 β†’ (βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣 ↔ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
1918cbvrexvw 3235 . . . . . . . . . . . . . . . . . 18 (βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣 ↔ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣)
2017, 19anbi12i 627 . . . . . . . . . . . . . . . . 17 ((βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
2115, 20sylib 217 . . . . . . . . . . . . . . . 16 (βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) β†’ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
22 reeanv 3226 . . . . . . . . . . . . . . . . 17 (βˆƒπ‘“ ∈ 𝐿 βˆƒπ‘” ∈ 𝐿 (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
23 txflf.l . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐿 ∈ (Filβ€˜π‘))
24 filin 23357 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Filβ€˜π‘) ∧ 𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿) β†’ (𝑓 ∩ 𝑔) ∈ 𝐿)
25243expb 1120 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ (Filβ€˜π‘) ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) β†’ (𝑓 ∩ 𝑔) ∈ 𝐿)
2623, 25sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) β†’ (𝑓 ∩ 𝑔) ∈ 𝐿)
27 inss1 4228 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 ∩ 𝑔) βŠ† 𝑓
28 ssralv 4050 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∩ 𝑔) βŠ† 𝑓 β†’ (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 β†’ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒))
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 β†’ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒)
30 inss2 4229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 ∩ 𝑔) βŠ† 𝑔
31 ssralv 4050 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∩ 𝑔) βŠ† 𝑔 β†’ (βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣 β†’ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣))
3230, 31ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣 β†’ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣)
3329, 32anim12i 613 . . . . . . . . . . . . . . . . . . . 20 ((βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) β†’ (βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣))
34 raleq 3322 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž = (𝑓 ∩ 𝑔) β†’ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ↔ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒))
35 raleq 3322 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž = (𝑓 ∩ 𝑔) β†’ (βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣 ↔ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣))
3634, 35anbi12d 631 . . . . . . . . . . . . . . . . . . . . 21 (β„Ž = (𝑓 ∩ 𝑔) β†’ ((βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣)))
3736rspcev 3612 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∩ 𝑔) ∈ 𝐿 ∧ (βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣)) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
3826, 33, 37syl2an 596 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) ∧ (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣)) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
3938ex 413 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) β†’ ((βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
4039rexlimdvva 3211 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆƒπ‘“ ∈ 𝐿 βˆƒπ‘” ∈ 𝐿 (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
4122, 40biimtrrid 242 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
4221, 41impbid2 225 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣)))
43 df-ima 5689 . . . . . . . . . . . . . . . . . . 19 (𝐻 β€œ β„Ž) = ran (𝐻 β†Ύ β„Ž)
44 filelss 23355 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Filβ€˜π‘) ∧ β„Ž ∈ 𝐿) β†’ β„Ž βŠ† 𝑍)
4523, 44sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ β„Ž βŠ† 𝑍)
46 txflf.h . . . . . . . . . . . . . . . . . . . . . . 23 𝐻 = (𝑛 ∈ 𝑍 ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩)
4746reseq1i 5977 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻 β†Ύ β„Ž) = ((𝑛 ∈ 𝑍 ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) β†Ύ β„Ž)
48 resmpt 6037 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž βŠ† 𝑍 β†’ ((𝑛 ∈ 𝑍 ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) β†Ύ β„Ž) = (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
4947, 48eqtrid 2784 . . . . . . . . . . . . . . . . . . . . 21 (β„Ž βŠ† 𝑍 β†’ (𝐻 β†Ύ β„Ž) = (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
5045, 49syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ (𝐻 β†Ύ β„Ž) = (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
5150rneqd 5937 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ ran (𝐻 β†Ύ β„Ž) = ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
5243, 51eqtrid 2784 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ (𝐻 β€œ β„Ž) = ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
5352sseq1d 4013 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ ((𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣) ↔ ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣)))
54 opelxp 5712 . . . . . . . . . . . . . . . . . . 19 (⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑒 Γ— 𝑣) ↔ ((πΉβ€˜π‘›) ∈ 𝑒 ∧ (πΊβ€˜π‘›) ∈ 𝑣))
5554ralbii 3093 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘› ∈ β„Ž ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑒 Γ— 𝑣) ↔ βˆ€π‘› ∈ β„Ž ((πΉβ€˜π‘›) ∈ 𝑒 ∧ (πΊβ€˜π‘›) ∈ 𝑣))
56 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) = (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩)
5756fmpt 7109 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘› ∈ β„Ž ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑒 Γ— 𝑣) ↔ (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩):β„ŽβŸΆ(𝑒 Γ— 𝑣))
58 opex 5464 . . . . . . . . . . . . . . . . . . . . 21 ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ V
5958, 56fnmpti 6693 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) Fn β„Ž
60 df-f 6547 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩):β„ŽβŸΆ(𝑒 Γ— 𝑣) ↔ ((𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) Fn β„Ž ∧ ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣)))
6159, 60mpbiran 707 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩):β„ŽβŸΆ(𝑒 Γ— 𝑣) ↔ ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣))
6257, 61bitri 274 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘› ∈ β„Ž ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑒 Γ— 𝑣) ↔ ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣))
63 r19.26 3111 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘› ∈ β„Ž ((πΉβ€˜π‘›) ∈ 𝑒 ∧ (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
6455, 62, 633bitr3i 300 . . . . . . . . . . . . . . . . 17 (ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣) ↔ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
6553, 64bitrdi 286 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ ((𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣) ↔ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
6665rexbidva 3176 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣) ↔ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
67 txflf.f . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐹:π‘βŸΆπ‘‹)
6867adantr 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ 𝐹:π‘βŸΆπ‘‹)
6968ffund 6721 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ Fun 𝐹)
70 filelss 23355 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Filβ€˜π‘) ∧ 𝑓 ∈ 𝐿) β†’ 𝑓 βŠ† 𝑍)
7123, 70sylan 580 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ 𝑓 βŠ† 𝑍)
7268fdmd 6728 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ dom 𝐹 = 𝑍)
7371, 72sseqtrrd 4023 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ 𝑓 βŠ† dom 𝐹)
74 funimass4 6956 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐹 ∧ 𝑓 βŠ† dom 𝐹) β†’ ((𝐹 β€œ 𝑓) βŠ† 𝑒 ↔ βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒))
7569, 73, 74syl2anc 584 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ ((𝐹 β€œ 𝑓) βŠ† 𝑒 ↔ βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒))
7675rexbidva 3176 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ↔ βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒))
77 txflf.g . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐺:π‘βŸΆπ‘Œ)
7877adantr 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ 𝐺:π‘βŸΆπ‘Œ)
7978ffund 6721 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ Fun 𝐺)
80 filelss 23355 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Filβ€˜π‘) ∧ 𝑔 ∈ 𝐿) β†’ 𝑔 βŠ† 𝑍)
8123, 80sylan 580 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ 𝑔 βŠ† 𝑍)
8278fdmd 6728 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ dom 𝐺 = 𝑍)
8381, 82sseqtrrd 4023 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ 𝑔 βŠ† dom 𝐺)
84 funimass4 6956 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐺 ∧ 𝑔 βŠ† dom 𝐺) β†’ ((𝐺 β€œ 𝑔) βŠ† 𝑣 ↔ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
8579, 83, 84syl2anc 584 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ ((𝐺 β€œ 𝑔) βŠ† 𝑣 ↔ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
8685rexbidva 3176 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣 ↔ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
8776, 86anbi12d 631 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣)))
8842, 66, 873bitr4d 310 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
8914, 88imbi12d 344 . . . . . . . . . . . . 13 (πœ‘ β†’ ((βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ ((𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑒) β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
90 impexp 451 . . . . . . . . . . . . 13 (((𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑒) β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)) ↔ (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
9189, 90bitrdi 286 . . . . . . . . . . . 12 (πœ‘ β†’ ((βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))))
9291ralbidv 3177 . . . . . . . . . . 11 (πœ‘ β†’ (βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))))
93 eleq2 2822 . . . . . . . . . . . . 13 (π‘₯ = 𝑣 β†’ (𝑆 ∈ π‘₯ ↔ 𝑆 ∈ 𝑣))
9493ralrab 3689 . . . . . . . . . . . 12 (βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)) ↔ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
95 r19.21v 3179 . . . . . . . . . . . 12 (βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)) ↔ (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
9694, 95bitr3i 276 . . . . . . . . . . 11 (βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))) ↔ (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
9792, 96bitrdi 286 . . . . . . . . . 10 (πœ‘ β†’ (βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
9897ralbidv 3177 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
99 eleq2 2822 . . . . . . . . . 10 (π‘₯ = 𝑒 β†’ (𝑅 ∈ π‘₯ ↔ 𝑅 ∈ 𝑒))
10099ralrab 3689 . . . . . . . . 9 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
10198, 100bitr4di 288 . . . . . . . 8 (πœ‘ β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
102101adantr 481 . . . . . . 7 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
103 txflf.j . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
104 toponmax 22427 . . . . . . . . . . 11 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 ∈ 𝐽)
105103, 104syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ 𝐽)
106 eleq2 2822 . . . . . . . . . . . 12 (π‘₯ = 𝑋 β†’ (𝑅 ∈ π‘₯ ↔ 𝑅 ∈ 𝑋))
107106rspcev 3612 . . . . . . . . . . 11 ((𝑋 ∈ 𝐽 ∧ 𝑅 ∈ 𝑋) β†’ βˆƒπ‘₯ ∈ 𝐽 𝑅 ∈ π‘₯)
108 rabn0 4385 . . . . . . . . . . 11 ({π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ… ↔ βˆƒπ‘₯ ∈ 𝐽 𝑅 ∈ π‘₯)
109107, 108sylibr 233 . . . . . . . . . 10 ((𝑋 ∈ 𝐽 ∧ 𝑅 ∈ 𝑋) β†’ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ…)
110105, 109sylan 580 . . . . . . . . 9 ((πœ‘ ∧ 𝑅 ∈ 𝑋) β†’ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ…)
111 txflf.k . . . . . . . . . . 11 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
112 toponmax 22427 . . . . . . . . . . 11 (𝐾 ∈ (TopOnβ€˜π‘Œ) β†’ π‘Œ ∈ 𝐾)
113111, 112syl 17 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ 𝐾)
114 eleq2 2822 . . . . . . . . . . . 12 (π‘₯ = π‘Œ β†’ (𝑆 ∈ π‘₯ ↔ 𝑆 ∈ π‘Œ))
115114rspcev 3612 . . . . . . . . . . 11 ((π‘Œ ∈ 𝐾 ∧ 𝑆 ∈ π‘Œ) β†’ βˆƒπ‘₯ ∈ 𝐾 𝑆 ∈ π‘₯)
116 rabn0 4385 . . . . . . . . . . 11 ({π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ… ↔ βˆƒπ‘₯ ∈ 𝐾 𝑆 ∈ π‘₯)
117115, 116sylibr 233 . . . . . . . . . 10 ((π‘Œ ∈ 𝐾 ∧ 𝑆 ∈ π‘Œ) β†’ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ…)
118113, 117sylan 580 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 ∈ π‘Œ) β†’ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ…)
119110, 118anim12dan 619 . . . . . . . 8 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ ({π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ… ∧ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ…))
120 r19.28zv 4500 . . . . . . . . . 10 ({π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ… β†’ (βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
121120ralbidv 3177 . . . . . . . . 9 ({π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ… β†’ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
122 r19.27zv 4505 . . . . . . . . 9 ({π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ… β†’ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
123121, 122sylan9bbr 511 . . . . . . . 8 (({π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ… ∧ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ…) β†’ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
124119, 123syl 17 . . . . . . 7 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
125102, 124bitrd 278 . . . . . 6 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
12699ralrab 3689 . . . . . . 7 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ↔ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒))
12793ralrab 3689 . . . . . . 7 (βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣 ↔ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))
128126, 127anbi12i 627 . . . . . 6 ((βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
129125, 128bitrdi 286 . . . . 5 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
13011, 129bitrid 282 . . . 4 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧) ↔ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
131130pm5.32da 579 . . 3 (πœ‘ β†’ (((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ) ∧ βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ) ∧ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))))
132 opelxp 5712 . . . 4 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑋 Γ— π‘Œ) ↔ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ))
133132anbi1i 624 . . 3 ((βŸ¨π‘…, π‘†βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ) ∧ βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧)))
134 an4 654 . . 3 (((𝑅 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒)) ∧ (𝑆 ∈ π‘Œ ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ) ∧ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
135131, 133, 1343bitr4g 313 . 2 (πœ‘ β†’ ((βŸ¨π‘…, π‘†βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒)) ∧ (𝑆 ∈ π‘Œ ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))))
136 eqid 2732 . . . . . . . 8 ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣)) = ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))
137136txval 23067 . . . . . . 7 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐽 Γ—t 𝐾) = (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))))
138103, 111, 137syl2anc 584 . . . . . 6 (πœ‘ β†’ (𝐽 Γ—t 𝐾) = (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))))
139138oveq1d 7423 . . . . 5 (πœ‘ β†’ ((𝐽 Γ—t 𝐾) fLimf 𝐿) = ((topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) fLimf 𝐿))
140139fveq1d 6893 . . . 4 (πœ‘ β†’ (((𝐽 Γ—t 𝐾) fLimf 𝐿)β€˜π») = (((topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) fLimf 𝐿)β€˜π»))
141140eleq2d 2819 . . 3 (πœ‘ β†’ (βŸ¨π‘…, π‘†βŸ© ∈ (((𝐽 Γ—t 𝐾) fLimf 𝐿)β€˜π») ↔ βŸ¨π‘…, π‘†βŸ© ∈ (((topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) fLimf 𝐿)β€˜π»)))
142 txtopon 23094 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
143103, 111, 142syl2anc 584 . . . . 5 (πœ‘ β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
144138, 143eqeltrrd 2834 . . . 4 (πœ‘ β†’ (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
14567ffvelcdmda 7086 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›) ∈ 𝑋)
14677ffvelcdmda 7086 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΊβ€˜π‘›) ∈ π‘Œ)
147145, 146opelxpd 5715 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑋 Γ— π‘Œ))
148147, 46fmptd 7113 . . . 4 (πœ‘ β†’ 𝐻:π‘βŸΆ(𝑋 Γ— π‘Œ))
149 eqid 2732 . . . . 5 (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) = (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣)))
150149flftg 23499 . . . 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 23496 . . . 4 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐿 ∈ (Filβ€˜π‘) ∧ 𝐹:π‘βŸΆπ‘‹) β†’ (𝑅 ∈ ((𝐽 fLimf 𝐿)β€˜πΉ) ↔ (𝑅 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒))))
154103, 23, 67, 153syl3anc 1371 . . 3 (πœ‘ β†’ (𝑅 ∈ ((𝐽 fLimf 𝐿)β€˜πΉ) ↔ (𝑅 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒))))
155 isflf 23496 . . . 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 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  βŸ¨cop 4634   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7408   ∈ cmpo 7410  topGenctg 17382  TopOnctopon 22411   Γ—t ctx 23063  Filcfil 23348   fLimf cflf 23438
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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-map 8821  df-topgen 17388  df-fbas 20940  df-fg 20941  df-top 22395  df-topon 22412  df-bases 22448  df-ntr 22523  df-nei 22601  df-tx 23065  df-fil 23349  df-fm 23441  df-flim 23442  df-flf 23443
This theorem is referenced by:  flfcnp2  23510
  Copyright terms: Public domain W3C validator