Metamath Proof Explorer


Theorem txflf

Description: Two sequences converge in a filter iff the sequence of their ordered pairs converges. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses txflf.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
txflf.k ( 𝜑𝐾 ∈ ( TopOn ‘ 𝑌 ) )
txflf.l ( 𝜑𝐿 ∈ ( Fil ‘ 𝑍 ) )
txflf.f ( 𝜑𝐹 : 𝑍𝑋 )
txflf.g ( 𝜑𝐺 : 𝑍𝑌 )
txflf.h 𝐻 = ( 𝑛𝑍 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ )
Assertion txflf ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ 𝐻 ) ↔ ( 𝑅 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝑆 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 txflf.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 txflf.k ( 𝜑𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 txflf.l ( 𝜑𝐿 ∈ ( Fil ‘ 𝑍 ) )
4 txflf.f ( 𝜑𝐹 : 𝑍𝑋 )
5 txflf.g ( 𝜑𝐺 : 𝑍𝑌 )
6 txflf.h 𝐻 = ( 𝑛𝑍 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ )
7 vex 𝑢 ∈ V
8 vex 𝑣 ∈ V
9 7 8 xpex ( 𝑢 × 𝑣 ) ∈ V
10 9 rgen2w 𝑢𝐽𝑣𝐾 ( 𝑢 × 𝑣 ) ∈ V
11 eqid ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) = ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) )
12 eleq2 ( 𝑧 = ( 𝑢 × 𝑣 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 ↔ ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ) )
13 sseq2 ( 𝑧 = ( 𝑢 × 𝑣 ) → ( ( 𝐻 ) ⊆ 𝑧 ↔ ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) )
14 13 rexbidv ( 𝑧 = ( 𝑢 × 𝑣 ) → ( ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ↔ ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) )
15 12 14 imbi12d ( 𝑧 = ( 𝑢 × 𝑣 ) → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ) )
16 11 15 ralrnmpo ( ∀ 𝑢𝐽𝑣𝐾 ( 𝑢 × 𝑣 ) ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ↔ ∀ 𝑢𝐽𝑣𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ) )
17 10 16 ax-mp ( ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ↔ ∀ 𝑢𝐽𝑣𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) )
18 opelxp ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ( 𝑅𝑢𝑆𝑣 ) )
19 18 biancomi ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ( 𝑆𝑣𝑅𝑢 ) )
20 19 a1i ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ( 𝑆𝑣𝑅𝑢 ) ) )
21 r19.40 ( ∃ 𝐿 ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) → ( ∃ 𝐿𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∃ 𝐿𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) )
22 raleq ( = 𝑓 → ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ↔ ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ) )
23 22 cbvrexvw ( ∃ 𝐿𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ↔ ∃ 𝑓𝐿𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 )
24 raleq ( = 𝑔 → ( ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ↔ ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) )
25 24 cbvrexvw ( ∃ 𝐿𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ↔ ∃ 𝑔𝐿𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 )
26 23 25 anbi12i ( ( ∃ 𝐿𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∃ 𝐿𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) ↔ ( ∃ 𝑓𝐿𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∃ 𝑔𝐿𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) )
27 21 26 sylib ( ∃ 𝐿 ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) → ( ∃ 𝑓𝐿𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∃ 𝑔𝐿𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) )
28 reeanv ( ∃ 𝑓𝐿𝑔𝐿 ( ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) ↔ ( ∃ 𝑓𝐿𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∃ 𝑔𝐿𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) )
29 filin ( ( 𝐿 ∈ ( Fil ‘ 𝑍 ) ∧ 𝑓𝐿𝑔𝐿 ) → ( 𝑓𝑔 ) ∈ 𝐿 )
30 29 3expb ( ( 𝐿 ∈ ( Fil ‘ 𝑍 ) ∧ ( 𝑓𝐿𝑔𝐿 ) ) → ( 𝑓𝑔 ) ∈ 𝐿 )
31 3 30 sylan ( ( 𝜑 ∧ ( 𝑓𝐿𝑔𝐿 ) ) → ( 𝑓𝑔 ) ∈ 𝐿 )
32 inss1 ( 𝑓𝑔 ) ⊆ 𝑓
33 ssralv ( ( 𝑓𝑔 ) ⊆ 𝑓 → ( ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 → ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐹𝑛 ) ∈ 𝑢 ) )
34 32 33 ax-mp ( ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 → ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐹𝑛 ) ∈ 𝑢 )
35 inss2 ( 𝑓𝑔 ) ⊆ 𝑔
36 ssralv ( ( 𝑓𝑔 ) ⊆ 𝑔 → ( ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 → ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐺𝑛 ) ∈ 𝑣 ) )
37 35 36 ax-mp ( ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 → ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐺𝑛 ) ∈ 𝑣 )
38 34 37 anim12i ( ( ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) → ( ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐺𝑛 ) ∈ 𝑣 ) )
39 raleq ( = ( 𝑓𝑔 ) → ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ↔ ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐹𝑛 ) ∈ 𝑢 ) )
40 raleq ( = ( 𝑓𝑔 ) → ( ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ↔ ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐺𝑛 ) ∈ 𝑣 ) )
41 39 40 anbi12d ( = ( 𝑓𝑔 ) → ( ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) ↔ ( ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐺𝑛 ) ∈ 𝑣 ) ) )
42 41 rspcev ( ( ( 𝑓𝑔 ) ∈ 𝐿 ∧ ( ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ∈ ( 𝑓𝑔 ) ( 𝐺𝑛 ) ∈ 𝑣 ) ) → ∃ 𝐿 ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) )
43 31 38 42 syl2an ( ( ( 𝜑 ∧ ( 𝑓𝐿𝑔𝐿 ) ) ∧ ( ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) ) → ∃ 𝐿 ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) )
44 43 ex ( ( 𝜑 ∧ ( 𝑓𝐿𝑔𝐿 ) ) → ( ( ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) → ∃ 𝐿 ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) ) )
45 44 rexlimdvva ( 𝜑 → ( ∃ 𝑓𝐿𝑔𝐿 ( ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) → ∃ 𝐿 ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) ) )
46 28 45 syl5bir ( 𝜑 → ( ( ∃ 𝑓𝐿𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∃ 𝑔𝐿𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) → ∃ 𝐿 ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) ) )
47 27 46 impbid2 ( 𝜑 → ( ∃ 𝐿 ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) ↔ ( ∃ 𝑓𝐿𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∃ 𝑔𝐿𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) ) )
48 df-ima ( 𝐻 ) = ran ( 𝐻 )
49 filelss ( ( 𝐿 ∈ ( Fil ‘ 𝑍 ) ∧ 𝐿 ) → 𝑍 )
50 3 49 sylan ( ( 𝜑𝐿 ) → 𝑍 )
51 6 reseq1i ( 𝐻 ) = ( ( 𝑛𝑍 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) ↾ )
52 resmpt ( 𝑍 → ( ( 𝑛𝑍 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) ↾ ) = ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) )
53 51 52 syl5eq ( 𝑍 → ( 𝐻 ) = ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) )
54 50 53 syl ( ( 𝜑𝐿 ) → ( 𝐻 ) = ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) )
55 54 rneqd ( ( 𝜑𝐿 ) → ran ( 𝐻 ) = ran ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) )
56 48 55 syl5eq ( ( 𝜑𝐿 ) → ( 𝐻 ) = ran ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) )
57 56 sseq1d ( ( 𝜑𝐿 ) → ( ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ↔ ran ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) ⊆ ( 𝑢 × 𝑣 ) ) )
58 opelxp ( ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ( ( 𝐹𝑛 ) ∈ 𝑢 ∧ ( 𝐺𝑛 ) ∈ 𝑣 ) )
59 58 ralbii ( ∀ 𝑛 ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ∀ 𝑛 ( ( 𝐹𝑛 ) ∈ 𝑢 ∧ ( 𝐺𝑛 ) ∈ 𝑣 ) )
60 eqid ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) = ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ )
61 60 fmpt ( ∀ 𝑛 ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) : ⟶ ( 𝑢 × 𝑣 ) )
62 opex ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ∈ V
63 62 60 fnmpti ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) Fn
64 df-f ( ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) : ⟶ ( 𝑢 × 𝑣 ) ↔ ( ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) Fn ∧ ran ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) ⊆ ( 𝑢 × 𝑣 ) ) )
65 63 64 mpbiran ( ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) : ⟶ ( 𝑢 × 𝑣 ) ↔ ran ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) ⊆ ( 𝑢 × 𝑣 ) )
66 61 65 bitri ( ∀ 𝑛 ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ran ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) ⊆ ( 𝑢 × 𝑣 ) )
67 r19.26 ( ∀ 𝑛 ( ( 𝐹𝑛 ) ∈ 𝑢 ∧ ( 𝐺𝑛 ) ∈ 𝑣 ) ↔ ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) )
68 59 66 67 3bitr3i ( ran ( 𝑛 ↦ ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ) ⊆ ( 𝑢 × 𝑣 ) ↔ ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) )
69 57 68 bitrdi ( ( 𝜑𝐿 ) → ( ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ↔ ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) ) )
70 69 rexbidva ( 𝜑 → ( ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ↔ ∃ 𝐿 ( ∀ 𝑛 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∀ 𝑛 ( 𝐺𝑛 ) ∈ 𝑣 ) ) )
71 4 adantr ( ( 𝜑𝑓𝐿 ) → 𝐹 : 𝑍𝑋 )
72 71 ffund ( ( 𝜑𝑓𝐿 ) → Fun 𝐹 )
73 filelss ( ( 𝐿 ∈ ( Fil ‘ 𝑍 ) ∧ 𝑓𝐿 ) → 𝑓𝑍 )
74 3 73 sylan ( ( 𝜑𝑓𝐿 ) → 𝑓𝑍 )
75 71 fdmd ( ( 𝜑𝑓𝐿 ) → dom 𝐹 = 𝑍 )
76 74 75 sseqtrrd ( ( 𝜑𝑓𝐿 ) → 𝑓 ⊆ dom 𝐹 )
77 funimass4 ( ( Fun 𝐹𝑓 ⊆ dom 𝐹 ) → ( ( 𝐹𝑓 ) ⊆ 𝑢 ↔ ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ) )
78 72 76 77 syl2anc ( ( 𝜑𝑓𝐿 ) → ( ( 𝐹𝑓 ) ⊆ 𝑢 ↔ ∀ 𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ) )
79 78 rexbidva ( 𝜑 → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ↔ ∃ 𝑓𝐿𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ) )
80 5 adantr ( ( 𝜑𝑔𝐿 ) → 𝐺 : 𝑍𝑌 )
81 80 ffund ( ( 𝜑𝑔𝐿 ) → Fun 𝐺 )
82 filelss ( ( 𝐿 ∈ ( Fil ‘ 𝑍 ) ∧ 𝑔𝐿 ) → 𝑔𝑍 )
83 3 82 sylan ( ( 𝜑𝑔𝐿 ) → 𝑔𝑍 )
84 80 fdmd ( ( 𝜑𝑔𝐿 ) → dom 𝐺 = 𝑍 )
85 83 84 sseqtrrd ( ( 𝜑𝑔𝐿 ) → 𝑔 ⊆ dom 𝐺 )
86 funimass4 ( ( Fun 𝐺𝑔 ⊆ dom 𝐺 ) → ( ( 𝐺𝑔 ) ⊆ 𝑣 ↔ ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) )
87 81 85 86 syl2anc ( ( 𝜑𝑔𝐿 ) → ( ( 𝐺𝑔 ) ⊆ 𝑣 ↔ ∀ 𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) )
88 87 rexbidva ( 𝜑 → ( ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ↔ ∃ 𝑔𝐿𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) )
89 79 88 anbi12d ( 𝜑 → ( ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ↔ ( ∃ 𝑓𝐿𝑛𝑓 ( 𝐹𝑛 ) ∈ 𝑢 ∧ ∃ 𝑔𝐿𝑛𝑔 ( 𝐺𝑛 ) ∈ 𝑣 ) ) )
90 47 70 89 3bitr4d ( 𝜑 → ( ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ↔ ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
91 20 90 imbi12d ( 𝜑 → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ↔ ( ( 𝑆𝑣𝑅𝑢 ) → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
92 impexp ( ( ( 𝑆𝑣𝑅𝑢 ) → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ↔ ( 𝑆𝑣 → ( 𝑅𝑢 → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
93 91 92 bitrdi ( 𝜑 → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ↔ ( 𝑆𝑣 → ( 𝑅𝑢 → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) ) )
94 93 ralbidv ( 𝜑 → ( ∀ 𝑣𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ↔ ∀ 𝑣𝐾 ( 𝑆𝑣 → ( 𝑅𝑢 → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) ) )
95 eleq2 ( 𝑥 = 𝑣 → ( 𝑆𝑥𝑆𝑣 ) )
96 95 ralrab ( ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( 𝑅𝑢 → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ↔ ∀ 𝑣𝐾 ( 𝑆𝑣 → ( 𝑅𝑢 → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
97 r19.21v ( ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( 𝑅𝑢 → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ↔ ( 𝑅𝑢 → ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
98 96 97 bitr3i ( ∀ 𝑣𝐾 ( 𝑆𝑣 → ( 𝑅𝑢 → ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) ↔ ( 𝑅𝑢 → ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
99 94 98 bitrdi ( 𝜑 → ( ∀ 𝑣𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ↔ ( 𝑅𝑢 → ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
100 99 ralbidv ( 𝜑 → ( ∀ 𝑢𝐽𝑣𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ↔ ∀ 𝑢𝐽 ( 𝑅𝑢 → ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
101 eleq2 ( 𝑥 = 𝑢 → ( 𝑅𝑥𝑅𝑢 ) )
102 101 ralrab ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ↔ ∀ 𝑢𝐽 ( 𝑅𝑢 → ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
103 100 102 bitr4di ( 𝜑 → ( ∀ 𝑢𝐽𝑣𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ↔ ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
104 103 adantr ( ( 𝜑 ∧ ( 𝑅𝑋𝑆𝑌 ) ) → ( ∀ 𝑢𝐽𝑣𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ↔ ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
105 toponmax ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋𝐽 )
106 1 105 syl ( 𝜑𝑋𝐽 )
107 eleq2 ( 𝑥 = 𝑋 → ( 𝑅𝑥𝑅𝑋 ) )
108 107 rspcev ( ( 𝑋𝐽𝑅𝑋 ) → ∃ 𝑥𝐽 𝑅𝑥 )
109 rabn0 ( { 𝑥𝐽𝑅𝑥 } ≠ ∅ ↔ ∃ 𝑥𝐽 𝑅𝑥 )
110 108 109 sylibr ( ( 𝑋𝐽𝑅𝑋 ) → { 𝑥𝐽𝑅𝑥 } ≠ ∅ )
111 106 110 sylan ( ( 𝜑𝑅𝑋 ) → { 𝑥𝐽𝑅𝑥 } ≠ ∅ )
112 toponmax ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌𝐾 )
113 2 112 syl ( 𝜑𝑌𝐾 )
114 eleq2 ( 𝑥 = 𝑌 → ( 𝑆𝑥𝑆𝑌 ) )
115 114 rspcev ( ( 𝑌𝐾𝑆𝑌 ) → ∃ 𝑥𝐾 𝑆𝑥 )
116 rabn0 ( { 𝑥𝐾𝑆𝑥 } ≠ ∅ ↔ ∃ 𝑥𝐾 𝑆𝑥 )
117 115 116 sylibr ( ( 𝑌𝐾𝑆𝑌 ) → { 𝑥𝐾𝑆𝑥 } ≠ ∅ )
118 113 117 sylan ( ( 𝜑𝑆𝑌 ) → { 𝑥𝐾𝑆𝑥 } ≠ ∅ )
119 111 118 anim12dan ( ( 𝜑 ∧ ( 𝑅𝑋𝑆𝑌 ) ) → ( { 𝑥𝐽𝑅𝑥 } ≠ ∅ ∧ { 𝑥𝐾𝑆𝑥 } ≠ ∅ ) )
120 r19.28zv ( { 𝑥𝐾𝑆𝑥 } ≠ ∅ → ( ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ↔ ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
121 120 ralbidv ( { 𝑥𝐾𝑆𝑥 } ≠ ∅ → ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ↔ ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
122 r19.27zv ( { 𝑥𝐽𝑅𝑥 } ≠ ∅ → ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ↔ ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
123 121 122 sylan9bbr ( ( { 𝑥𝐽𝑅𝑥 } ≠ ∅ ∧ { 𝑥𝐾𝑆𝑥 } ≠ ∅ ) → ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ↔ ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
124 119 123 syl ( ( 𝜑 ∧ ( 𝑅𝑋𝑆𝑌 ) ) → ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ( ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ↔ ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
125 104 124 bitrd ( ( 𝜑 ∧ ( 𝑅𝑋𝑆𝑌 ) ) → ( ∀ 𝑢𝐽𝑣𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ↔ ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
126 101 ralrab ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ↔ ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) )
127 95 ralrab ( ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ↔ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) )
128 126 127 anbi12i ( ( ∀ 𝑢 ∈ { 𝑥𝐽𝑅𝑥 } ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ∧ ∀ 𝑣 ∈ { 𝑥𝐾𝑆𝑥 } ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ↔ ( ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) )
129 125 128 bitrdi ( ( 𝜑 ∧ ( 𝑅𝑋𝑆𝑌 ) ) → ( ∀ 𝑢𝐽𝑣𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) → ∃ 𝐿 ( 𝐻 ) ⊆ ( 𝑢 × 𝑣 ) ) ↔ ( ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
130 17 129 syl5bb ( ( 𝜑 ∧ ( 𝑅𝑋𝑆𝑌 ) ) → ( ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ↔ ( ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
131 130 pm5.32da ( 𝜑 → ( ( ( 𝑅𝑋𝑆𝑌 ) ∧ ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ) ↔ ( ( 𝑅𝑋𝑆𝑌 ) ∧ ( ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) ) )
132 opelxp ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝑅𝑋𝑆𝑌 ) )
133 132 anbi1i ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ) ↔ ( ( 𝑅𝑋𝑆𝑌 ) ∧ ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ) )
134 an4 ( ( ( 𝑅𝑋 ∧ ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ) ∧ ( 𝑆𝑌 ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) ↔ ( ( 𝑅𝑋𝑆𝑌 ) ∧ ( ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
135 131 133 134 3bitr4g ( 𝜑 → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ) ↔ ( ( 𝑅𝑋 ∧ ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ) ∧ ( 𝑆𝑌 ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) ) )
136 eqid ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) = ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) )
137 136 txval ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) = ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) )
138 1 2 137 syl2anc ( 𝜑 → ( 𝐽 ×t 𝐾 ) = ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) )
139 138 oveq1d ( 𝜑 → ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) = ( ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) fLimf 𝐿 ) )
140 139 fveq1d ( 𝜑 → ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ 𝐻 ) = ( ( ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) fLimf 𝐿 ) ‘ 𝐻 ) )
141 140 eleq2d ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ 𝐻 ) ↔ ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) fLimf 𝐿 ) ‘ 𝐻 ) ) )
142 txtopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
143 1 2 142 syl2anc ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
144 138 143 eqeltrrd ( 𝜑 → ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
145 4 ffvelrnda ( ( 𝜑𝑛𝑍 ) → ( 𝐹𝑛 ) ∈ 𝑋 )
146 5 ffvelrnda ( ( 𝜑𝑛𝑍 ) → ( 𝐺𝑛 ) ∈ 𝑌 )
147 145 146 opelxpd ( ( 𝜑𝑛𝑍 ) → ⟨ ( 𝐹𝑛 ) , ( 𝐺𝑛 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
148 147 6 fmptd ( 𝜑𝐻 : 𝑍 ⟶ ( 𝑋 × 𝑌 ) )
149 eqid ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) = ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) )
150 149 flftg ( ( ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( Fil ‘ 𝑍 ) ∧ 𝐻 : 𝑍 ⟶ ( 𝑋 × 𝑌 ) ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) fLimf 𝐿 ) ‘ 𝐻 ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ) ) )
151 144 3 148 150 syl3anc ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( topGen ‘ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) fLimf 𝐿 ) ‘ 𝐻 ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ) ) )
152 141 151 bitrd ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ 𝐻 ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ∀ 𝑧 ∈ ran ( 𝑢𝐽 , 𝑣𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑧 → ∃ 𝐿 ( 𝐻 ) ⊆ 𝑧 ) ) ) )
153 isflf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑍 ) ∧ 𝐹 : 𝑍𝑋 ) → ( 𝑅 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝑅𝑋 ∧ ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ) ) )
154 1 3 4 153 syl3anc ( 𝜑 → ( 𝑅 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝑅𝑋 ∧ ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ) ) )
155 isflf ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑍 ) ∧ 𝐺 : 𝑍𝑌 ) → ( 𝑆 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐺 ) ↔ ( 𝑆𝑌 ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
156 2 3 5 155 syl3anc ( 𝜑 → ( 𝑆 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐺 ) ↔ ( 𝑆𝑌 ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) )
157 154 156 anbi12d ( 𝜑 → ( ( 𝑅 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝑆 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐺 ) ) ↔ ( ( 𝑅𝑋 ∧ ∀ 𝑢𝐽 ( 𝑅𝑢 → ∃ 𝑓𝐿 ( 𝐹𝑓 ) ⊆ 𝑢 ) ) ∧ ( 𝑆𝑌 ∧ ∀ 𝑣𝐾 ( 𝑆𝑣 → ∃ 𝑔𝐿 ( 𝐺𝑔 ) ⊆ 𝑣 ) ) ) ) )
158 135 152 157 3bitr4d ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ 𝐻 ) ↔ ( 𝑅 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ∧ 𝑆 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐺 ) ) ) )