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

Theorem txflf 23380
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 3451 . . . . . . . 8 𝑒 ∈ V
2 vex 3451 . . . . . . . 8 𝑣 ∈ V
31, 2xpex 7691 . . . . . . 7 (𝑒 Γ— 𝑣) ∈ V
43rgen2w 3066 . . . . . 6 βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (𝑒 Γ— 𝑣) ∈ V
5 eqid 2733 . . . . . . 7 (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣)) = (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))
6 eleq2 2823 . . . . . . . 8 (𝑧 = (𝑒 Γ— 𝑣) β†’ (βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 ↔ βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣)))
7 sseq2 3974 . . . . . . . . 9 (𝑧 = (𝑒 Γ— 𝑣) β†’ ((𝐻 β€œ β„Ž) βŠ† 𝑧 ↔ (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)))
87rexbidv 3172 . . . . . . . 8 (𝑧 = (𝑒 Γ— 𝑣) β†’ (βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧 ↔ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)))
96, 8imbi12d 345 . . . . . . 7 (𝑧 = (𝑒 Γ— 𝑣) β†’ ((βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧) ↔ (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣))))
105, 9ralrnmpo 7498 . . . . . 6 (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (𝑒 Γ— 𝑣) ∈ V β†’ (βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧) ↔ βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣))))
114, 10ax-mp 5 . . . . 5 (βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧) ↔ βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)))
12 opelxp 5673 . . . . . . . . . . . . . . . 16 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) ↔ (𝑅 ∈ 𝑒 ∧ 𝑆 ∈ 𝑣))
1312biancomi 464 . . . . . . . . . . . . . . 15 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) ↔ (𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑒))
1413a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) ↔ (𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑒)))
15 r19.40 3119 . . . . . . . . . . . . . . . . 17 (βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) β†’ (βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
16 raleq 3308 . . . . . . . . . . . . . . . . . . 19 (β„Ž = 𝑓 β†’ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ↔ βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒))
1716cbvrexvw 3225 . . . . . . . . . . . . . . . . . 18 (βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ↔ βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒)
18 raleq 3308 . . . . . . . . . . . . . . . . . . 19 (β„Ž = 𝑔 β†’ (βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣 ↔ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
1918cbvrexvw 3225 . . . . . . . . . . . . . . . . . 18 (βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣 ↔ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣)
2017, 19anbi12i 628 . . . . . . . . . . . . . . . . 17 ((βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒβ„Ž ∈ 𝐿 βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
2115, 20sylib 217 . . . . . . . . . . . . . . . 16 (βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) β†’ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
22 reeanv 3216 . . . . . . . . . . . . . . . . 17 (βˆƒπ‘“ ∈ 𝐿 βˆƒπ‘” ∈ 𝐿 (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
23 txflf.l . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐿 ∈ (Filβ€˜π‘))
24 filin 23228 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Filβ€˜π‘) ∧ 𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿) β†’ (𝑓 ∩ 𝑔) ∈ 𝐿)
25243expb 1121 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ (Filβ€˜π‘) ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) β†’ (𝑓 ∩ 𝑔) ∈ 𝐿)
2623, 25sylan 581 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) β†’ (𝑓 ∩ 𝑔) ∈ 𝐿)
27 inss1 4192 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 ∩ 𝑔) βŠ† 𝑓
28 ssralv 4014 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∩ 𝑔) βŠ† 𝑓 β†’ (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 β†’ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒))
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 β†’ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒)
30 inss2 4193 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 ∩ 𝑔) βŠ† 𝑔
31 ssralv 4014 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∩ 𝑔) βŠ† 𝑔 β†’ (βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣 β†’ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣))
3230, 31ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣 β†’ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣)
3329, 32anim12i 614 . . . . . . . . . . . . . . . . . . . 20 ((βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) β†’ (βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣))
34 raleq 3308 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž = (𝑓 ∩ 𝑔) β†’ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ↔ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒))
35 raleq 3308 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž = (𝑓 ∩ 𝑔) β†’ (βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣 ↔ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣))
3634, 35anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (β„Ž = (𝑓 ∩ 𝑔) β†’ ((βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣)))
3736rspcev 3583 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∩ 𝑔) ∈ 𝐿 ∧ (βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ (𝑓 ∩ 𝑔)(πΊβ€˜π‘›) ∈ 𝑣)) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
3826, 33, 37syl2an 597 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) ∧ (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣)) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
3938ex 414 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) β†’ ((βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
4039rexlimdvva 3202 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆƒπ‘“ ∈ 𝐿 βˆƒπ‘” ∈ 𝐿 (βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
4122, 40biimtrrid 242 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
4221, 41impbid2 225 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣)))
43 df-ima 5650 . . . . . . . . . . . . . . . . . . 19 (𝐻 β€œ β„Ž) = ran (𝐻 β†Ύ β„Ž)
44 filelss 23226 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ (Filβ€˜π‘) ∧ β„Ž ∈ 𝐿) β†’ β„Ž βŠ† 𝑍)
4523, 44sylan 581 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ β„Ž βŠ† 𝑍)
46 txflf.h . . . . . . . . . . . . . . . . . . . . . . 23 𝐻 = (𝑛 ∈ 𝑍 ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩)
4746reseq1i 5937 . . . . . . . . . . . . . . . . . . . . . 22 (𝐻 β†Ύ β„Ž) = ((𝑛 ∈ 𝑍 ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) β†Ύ β„Ž)
48 resmpt 5995 . . . . . . . . . . . . . . . . . . . . . 22 (β„Ž βŠ† 𝑍 β†’ ((𝑛 ∈ 𝑍 ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) β†Ύ β„Ž) = (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
4947, 48eqtrid 2785 . . . . . . . . . . . . . . . . . . . . 21 (β„Ž βŠ† 𝑍 β†’ (𝐻 β†Ύ β„Ž) = (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
5045, 49syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ (𝐻 β†Ύ β„Ž) = (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
5150rneqd 5897 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ ran (𝐻 β†Ύ β„Ž) = ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
5243, 51eqtrid 2785 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ (𝐻 β€œ β„Ž) = ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩))
5352sseq1d 3979 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ ((𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣) ↔ ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣)))
54 opelxp 5673 . . . . . . . . . . . . . . . . . . 19 (⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑒 Γ— 𝑣) ↔ ((πΉβ€˜π‘›) ∈ 𝑒 ∧ (πΊβ€˜π‘›) ∈ 𝑣))
5554ralbii 3093 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘› ∈ β„Ž ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑒 Γ— 𝑣) ↔ βˆ€π‘› ∈ β„Ž ((πΉβ€˜π‘›) ∈ 𝑒 ∧ (πΊβ€˜π‘›) ∈ 𝑣))
56 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) = (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩)
5756fmpt 7062 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘› ∈ β„Ž ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑒 Γ— 𝑣) ↔ (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩):β„ŽβŸΆ(𝑒 Γ— 𝑣))
58 opex 5425 . . . . . . . . . . . . . . . . . . . . 21 ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ V
5958, 56fnmpti 6648 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) Fn β„Ž
60 df-f 6504 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩):β„ŽβŸΆ(𝑒 Γ— 𝑣) ↔ ((𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) Fn β„Ž ∧ ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣)))
6159, 60mpbiran 708 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩):β„ŽβŸΆ(𝑒 Γ— 𝑣) ↔ ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣))
6257, 61bitri 275 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘› ∈ β„Ž ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑒 Γ— 𝑣) ↔ ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣))
63 r19.26 3111 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘› ∈ β„Ž ((πΉβ€˜π‘›) ∈ 𝑒 ∧ (πΊβ€˜π‘›) ∈ 𝑣) ↔ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
6455, 62, 633bitr3i 301 . . . . . . . . . . . . . . . . 17 (ran (𝑛 ∈ β„Ž ↦ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩) βŠ† (𝑒 Γ— 𝑣) ↔ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣))
6553, 64bitrdi 287 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ β„Ž ∈ 𝐿) β†’ ((𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣) ↔ (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
6665rexbidva 3170 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣) ↔ βˆƒβ„Ž ∈ 𝐿 (βˆ€π‘› ∈ β„Ž (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆ€π‘› ∈ β„Ž (πΊβ€˜π‘›) ∈ 𝑣)))
67 txflf.f . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐹:π‘βŸΆπ‘‹)
6867adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ 𝐹:π‘βŸΆπ‘‹)
6968ffund 6676 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ Fun 𝐹)
70 filelss 23226 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Filβ€˜π‘) ∧ 𝑓 ∈ 𝐿) β†’ 𝑓 βŠ† 𝑍)
7123, 70sylan 581 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ 𝑓 βŠ† 𝑍)
7268fdmd 6683 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ dom 𝐹 = 𝑍)
7371, 72sseqtrrd 3989 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ 𝑓 βŠ† dom 𝐹)
74 funimass4 6911 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐹 ∧ 𝑓 βŠ† dom 𝐹) β†’ ((𝐹 β€œ 𝑓) βŠ† 𝑒 ↔ βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒))
7569, 73, 74syl2anc 585 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑓 ∈ 𝐿) β†’ ((𝐹 β€œ 𝑓) βŠ† 𝑒 ↔ βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒))
7675rexbidva 3170 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ↔ βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒))
77 txflf.g . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐺:π‘βŸΆπ‘Œ)
7877adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ 𝐺:π‘βŸΆπ‘Œ)
7978ffund 6676 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ Fun 𝐺)
80 filelss 23226 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ (Filβ€˜π‘) ∧ 𝑔 ∈ 𝐿) β†’ 𝑔 βŠ† 𝑍)
8123, 80sylan 581 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ 𝑔 βŠ† 𝑍)
8278fdmd 6683 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ dom 𝐺 = 𝑍)
8381, 82sseqtrrd 3989 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ 𝑔 βŠ† dom 𝐺)
84 funimass4 6911 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐺 ∧ 𝑔 βŠ† dom 𝐺) β†’ ((𝐺 β€œ 𝑔) βŠ† 𝑣 ↔ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
8579, 83, 84syl2anc 585 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑔 ∈ 𝐿) β†’ ((𝐺 β€œ 𝑔) βŠ† 𝑣 ↔ βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
8685rexbidva 3170 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣 ↔ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣))
8776, 86anbi12d 632 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 βˆ€π‘› ∈ 𝑓 (πΉβ€˜π‘›) ∈ 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 βˆ€π‘› ∈ 𝑔 (πΊβ€˜π‘›) ∈ 𝑣)))
8842, 66, 873bitr4d 311 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
8914, 88imbi12d 345 . . . . . . . . . . . . 13 (πœ‘ β†’ ((βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ ((𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑒) β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
90 impexp 452 . . . . . . . . . . . . 13 (((𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑒) β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)) ↔ (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
9189, 90bitrdi 287 . . . . . . . . . . . 12 (πœ‘ β†’ ((βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))))
9291ralbidv 3171 . . . . . . . . . . 11 (πœ‘ β†’ (βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))))
93 eleq2 2823 . . . . . . . . . . . . 13 (π‘₯ = 𝑣 β†’ (𝑆 ∈ π‘₯ ↔ 𝑆 ∈ 𝑣))
9493ralrab 3655 . . . . . . . . . . . 12 (βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)) ↔ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
95 r19.21v 3173 . . . . . . . . . . . 12 (βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)) ↔ (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
9694, 95bitr3i 277 . . . . . . . . . . 11 (βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ (𝑅 ∈ 𝑒 β†’ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))) ↔ (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
9792, 96bitrdi 287 . . . . . . . . . 10 (πœ‘ β†’ (βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
9897ralbidv 3171 . . . . . . . . 9 (πœ‘ β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
99 eleq2 2823 . . . . . . . . . 10 (π‘₯ = 𝑒 β†’ (𝑅 ∈ π‘₯ ↔ 𝑅 ∈ 𝑒))
10099ralrab 3655 . . . . . . . . 9 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
10198, 100bitr4di 289 . . . . . . . 8 (πœ‘ β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
102101adantr 482 . . . . . . 7 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
103 txflf.j . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
104 toponmax 22298 . . . . . . . . . . 11 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 ∈ 𝐽)
105103, 104syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ 𝐽)
106 eleq2 2823 . . . . . . . . . . . 12 (π‘₯ = 𝑋 β†’ (𝑅 ∈ π‘₯ ↔ 𝑅 ∈ 𝑋))
107106rspcev 3583 . . . . . . . . . . 11 ((𝑋 ∈ 𝐽 ∧ 𝑅 ∈ 𝑋) β†’ βˆƒπ‘₯ ∈ 𝐽 𝑅 ∈ π‘₯)
108 rabn0 4349 . . . . . . . . . . 11 ({π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ… ↔ βˆƒπ‘₯ ∈ 𝐽 𝑅 ∈ π‘₯)
109107, 108sylibr 233 . . . . . . . . . 10 ((𝑋 ∈ 𝐽 ∧ 𝑅 ∈ 𝑋) β†’ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ…)
110105, 109sylan 581 . . . . . . . . 9 ((πœ‘ ∧ 𝑅 ∈ 𝑋) β†’ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ…)
111 txflf.k . . . . . . . . . . 11 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
112 toponmax 22298 . . . . . . . . . . 11 (𝐾 ∈ (TopOnβ€˜π‘Œ) β†’ π‘Œ ∈ 𝐾)
113111, 112syl 17 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ 𝐾)
114 eleq2 2823 . . . . . . . . . . . 12 (π‘₯ = π‘Œ β†’ (𝑆 ∈ π‘₯ ↔ 𝑆 ∈ π‘Œ))
115114rspcev 3583 . . . . . . . . . . 11 ((π‘Œ ∈ 𝐾 ∧ 𝑆 ∈ π‘Œ) β†’ βˆƒπ‘₯ ∈ 𝐾 𝑆 ∈ π‘₯)
116 rabn0 4349 . . . . . . . . . . 11 ({π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ… ↔ βˆƒπ‘₯ ∈ 𝐾 𝑆 ∈ π‘₯)
117115, 116sylibr 233 . . . . . . . . . 10 ((π‘Œ ∈ 𝐾 ∧ 𝑆 ∈ π‘Œ) β†’ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ…)
118113, 117sylan 581 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 ∈ π‘Œ) β†’ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ…)
119110, 118anim12dan 620 . . . . . . . 8 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ ({π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ… ∧ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ…))
120 r19.28zv 4462 . . . . . . . . . 10 ({π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ… β†’ (βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
121120ralbidv 3171 . . . . . . . . 9 ({π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ… β†’ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
122 r19.27zv 4467 . . . . . . . . 9 ({π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ… β†’ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
123121, 122sylan9bbr 512 . . . . . . . 8 (({π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯} β‰  βˆ… ∧ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} β‰  βˆ…) β†’ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
124119, 123syl 17 . . . . . . 7 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯} (βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
125102, 124bitrd 279 . . . . . 6 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
12699ralrab 3655 . . . . . . 7 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ↔ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒))
12793ralrab 3655 . . . . . . 7 (βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣 ↔ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))
128126, 127anbi12i 628 . . . . . 6 ((βˆ€π‘’ ∈ {π‘₯ ∈ 𝐽 ∣ 𝑅 ∈ π‘₯}βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒 ∧ βˆ€π‘£ ∈ {π‘₯ ∈ 𝐾 ∣ 𝑆 ∈ π‘₯}βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣) ↔ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))
129125, 128bitrdi 287 . . . . 5 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘’ ∈ 𝐽 βˆ€π‘£ ∈ 𝐾 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑒 Γ— 𝑣) β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† (𝑒 Γ— 𝑣)) ↔ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
13011, 129bitrid 283 . . . 4 ((πœ‘ ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ)) β†’ (βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧) ↔ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
131130pm5.32da 580 . . 3 (πœ‘ β†’ (((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ) ∧ βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ) ∧ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))))
132 opelxp 5673 . . . 4 (βŸ¨π‘…, π‘†βŸ© ∈ (𝑋 Γ— π‘Œ) ↔ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ))
133132anbi1i 625 . . 3 ((βŸ¨π‘…, π‘†βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ) ∧ βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧)))
134 an4 655 . . 3 (((𝑅 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒)) ∧ (𝑆 ∈ π‘Œ ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ π‘Œ) ∧ (βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒) ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣))))
135131, 133, 1343bitr4g 314 . 2 (πœ‘ β†’ ((βŸ¨π‘…, π‘†βŸ© ∈ (𝑋 Γ— π‘Œ) ∧ βˆ€π‘§ ∈ ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))(βŸ¨π‘…, π‘†βŸ© ∈ 𝑧 β†’ βˆƒβ„Ž ∈ 𝐿 (𝐻 β€œ β„Ž) βŠ† 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒)) ∧ (𝑆 ∈ π‘Œ ∧ βˆ€π‘£ ∈ 𝐾 (𝑆 ∈ 𝑣 β†’ βˆƒπ‘” ∈ 𝐿 (𝐺 β€œ 𝑔) βŠ† 𝑣)))))
136 eqid 2733 . . . . . . . 8 ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣)) = ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))
137136txval 22938 . . . . . . 7 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐽 Γ—t 𝐾) = (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))))
138103, 111, 137syl2anc 585 . . . . . 6 (πœ‘ β†’ (𝐽 Γ—t 𝐾) = (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))))
139138oveq1d 7376 . . . . 5 (πœ‘ β†’ ((𝐽 Γ—t 𝐾) fLimf 𝐿) = ((topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) fLimf 𝐿))
140139fveq1d 6848 . . . 4 (πœ‘ β†’ (((𝐽 Γ—t 𝐾) fLimf 𝐿)β€˜π») = (((topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) fLimf 𝐿)β€˜π»))
141140eleq2d 2820 . . 3 (πœ‘ β†’ (βŸ¨π‘…, π‘†βŸ© ∈ (((𝐽 Γ—t 𝐾) fLimf 𝐿)β€˜π») ↔ βŸ¨π‘…, π‘†βŸ© ∈ (((topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) fLimf 𝐿)β€˜π»)))
142 txtopon 22965 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
143103, 111, 142syl2anc 585 . . . . 5 (πœ‘ β†’ (𝐽 Γ—t 𝐾) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
144138, 143eqeltrrd 2835 . . . 4 (πœ‘ β†’ (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
14567ffvelcdmda 7039 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›) ∈ 𝑋)
14677ffvelcdmda 7039 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΊβ€˜π‘›) ∈ π‘Œ)
147145, 146opelxpd 5675 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ ⟨(πΉβ€˜π‘›), (πΊβ€˜π‘›)⟩ ∈ (𝑋 Γ— π‘Œ))
148147, 46fmptd 7066 . . . 4 (πœ‘ β†’ 𝐻:π‘βŸΆ(𝑋 Γ— π‘Œ))
149 eqid 2733 . . . . 5 (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣))) = (topGenβ€˜ran (𝑒 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑒 Γ— 𝑣)))
150149flftg 23370 . . . 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 23367 . . . 4 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐿 ∈ (Filβ€˜π‘) ∧ 𝐹:π‘βŸΆπ‘‹) β†’ (𝑅 ∈ ((𝐽 fLimf 𝐿)β€˜πΉ) ↔ (𝑅 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒))))
154103, 23, 67, 153syl3anc 1372 . . 3 (πœ‘ β†’ (𝑅 ∈ ((𝐽 fLimf 𝐿)β€˜πΉ) ↔ (𝑅 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑅 ∈ 𝑒 β†’ βˆƒπ‘“ ∈ 𝐿 (𝐹 β€œ 𝑓) βŠ† 𝑒))))
155 isflf 23367 . . . 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 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3447   ∩ cin 3913   βŠ† wss 3914  βˆ…c0 4286  βŸ¨cop 4596   ↦ cmpt 5192   Γ— cxp 5635  dom cdm 5637  ran crn 5638   β†Ύ cres 5639   β€œ cima 5640  Fun wfun 6494   Fn wfn 6495  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361   ∈ cmpo 7363  topGenctg 17327  TopOnctopon 22282   Γ—t ctx 22934  Filcfil 23219   fLimf cflf 23309
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 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
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 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7925  df-2nd 7926  df-map 8773  df-topgen 17333  df-fbas 20816  df-fg 20817  df-top 22266  df-topon 22283  df-bases 22319  df-ntr 22394  df-nei 22472  df-tx 22936  df-fil 23220  df-fm 23312  df-flim 23313  df-flf 23314
This theorem is referenced by:  flfcnp2  23381
  Copyright terms: Public domain W3C validator