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 𝐿 ) ‘ 𝐺 ) ) ) )