Metamath Proof Explorer

Theorem txlm

Description: Two sequences converge iff the sequence of their ordered pairs converges. Proposition 14-2.6 of Gleason p. 230. (Contributed by NM, 16-Jul-2007) (Revised by Mario Carneiro, 5-May-2014)

Ref Expression
Hypotheses txlm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
txlm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
txlm.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
txlm.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
txlm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
txlm.g ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ 𝑌 )
txlm.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ )
Assertion txlm ( 𝜑 → ( ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑅 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐾 ) 𝑆 ) ↔ 𝐻 ( ⇝𝑡 ‘ ( 𝐽 ×t 𝐾 ) ) ⟨ 𝑅 , 𝑆 ⟩ ) )

Proof

Step Hyp Ref Expression
1 txlm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 txlm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 txlm.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 txlm.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
5 txlm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
6 txlm.g ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ 𝑌 )
7 txlm.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ )
8 r19.27v ⊢ ( ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∀ 𝑢 ∈ 𝐽 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
9 r19.28v ⊢ ( ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
10 9 ralimi ⊢ ( ∀ 𝑢 ∈ 𝐽 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
11 8 10 syl ⊢ ( ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
12 simprl ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ∧ ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ) ) → 𝑤 ∈ ( 𝐽 ×t 𝐾 ) )
13 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
14 3 13 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
15 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
16 4 15 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
17 eqid ⊢ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) = ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) )
18 17 txval ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ×t 𝐾 ) = ( topGen ‘ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) )
19 14 16 18 syl2anc ⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) = ( topGen ‘ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ∧ ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ) ) → ( 𝐽 ×t 𝐾 ) = ( topGen ‘ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) )
21 12 20 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ∧ ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ) ) → 𝑤 ∈ ( topGen ‘ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) )
22 simprr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ∧ ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ) ) → ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 )
23 tg2 ⊢ ( ( 𝑤 ∈ ( topGen ‘ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) ) ∧ ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ) → ∃ 𝑡 ∈ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤 ) )
24 21 22 23 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ∧ ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ) ) → ∃ 𝑡 ∈ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤 ) )
25 vex ⊢ 𝑢 ∈ V
26 vex ⊢ 𝑣 ∈ V
27 25 26 xpex ⊢ ( 𝑢 × 𝑣 ) ∈ V
28 27 rgen2w ⊢ ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( 𝑢 × 𝑣 ) ∈ V
29 eqid ⊢ ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) = ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) )
30 eleq2 ⊢ ( 𝑡 = ( 𝑢 × 𝑣 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑡 ↔ ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ) )
31 sseq1 ⊢ ( 𝑡 = ( 𝑢 × 𝑣 ) → ( 𝑡 ⊆ 𝑤 ↔ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) )
32 30 31 anbi12d ⊢ ( 𝑡 = ( 𝑢 × 𝑣 ) → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤 ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
33 29 32 rexrnmpo ⊢ ( ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( 𝑢 × 𝑣 ) ∈ V → ( ∃ 𝑡 ∈ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤 ) ↔ ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
34 28 33 ax-mp ⊢ ( ∃ 𝑡 ∈ ran ( 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐾 ↦ ( 𝑢 × 𝑣 ) ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤 ) ↔ ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) )
35 24 34 sylib ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ∧ ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) )
36 35 ex ⊢ ( 𝜑 → ( ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ∧ ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
37 r19.29 ⊢ ( ( ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ∃ 𝑢 ∈ 𝐽 ( ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
38 r19.29 ⊢ ( ( ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ∃ 𝑣 ∈ 𝐾 ( ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
39 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) )
40 opelxp ⊢ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ( 𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑣 ) )
41 39 40 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ( 𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑣 ) )
42 pm2.27 ⊢ ( 𝑅 ∈ 𝑢 → ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
43 pm2.27 ⊢ ( 𝑆 ∈ 𝑣 → ( ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) )
44 42 43 im2anan9 ⊢ ( ( 𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑣 ) → ( ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
45 41 44 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ( ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
46 1 rexanuz2 ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) )
47 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
48 opelxpi ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ⟨ ( 𝐹 ‘ 𝑘 ) , ( 𝐺 ‘ 𝑘 ) ⟩ ∈ ( 𝑢 × 𝑣 ) )
49 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
50 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
51 49 50 opeq12d ⊢ ( 𝑛 = 𝑘 → ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑘 ) , ( 𝐺 ‘ 𝑘 ) ⟩ )
52 opex ⊢ ⟨ ( 𝐹 ‘ 𝑘 ) , ( 𝐺 ‘ 𝑘 ) ⟩ ∈ V
53 51 7 52 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( 𝐻 ‘ 𝑘 ) = ⟨ ( 𝐹 ‘ 𝑘 ) , ( 𝐺 ‘ 𝑘 ) ⟩ )
54 53 eleq1d ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑣 ) ↔ ⟨ ( 𝐹 ‘ 𝑘 ) , ( 𝐺 ‘ 𝑘 ) ⟩ ∈ ( 𝑢 × 𝑣 ) ) )
55 48 54 imbitrrid ⊢ ( 𝑘 ∈ 𝑍 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑣 ) ) )
56 55 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑣 ) ) )
57 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑢 × 𝑣 ) ⊆ 𝑤 )
58 57 sseld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑣 ) → ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
59 56 58 syld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
60 47 59 sylan2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
61 60 anassrs ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
62 61 ralimdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
63 62 reximdva ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
64 46 63 biimtrrid ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ( ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
65 45 64 syld ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ( ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
66 65 ex ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ( ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
67 66 impcomd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐾 ) → ( ( ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
68 67 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ∃ 𝑣 ∈ 𝐾 ( ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
69 38 68 syl5 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ( ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
70 69 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝐽 ( ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
71 37 70 syl5 ⊢ ( 𝜑 → ( ( ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ∧ ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) )
72 71 expcomd ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ( ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
73 36 72 syld ⊢ ( 𝜑 → ( ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ∧ ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ) → ( ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
74 73 expdimp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ( ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
75 74 com23 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → ( ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
76 75 ralrimdva ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝐽 ∀ 𝑣 ∈ 𝐾 ( ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
77 11 76 syl5 ⊢ ( 𝜑 → ( ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
78 77 adantr ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ) → ( ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
79 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → 𝐽 ∈ Top )
80 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → 𝐾 ∈ Top )
81 simprr ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → 𝑢 ∈ 𝐽 )
82 toponmax ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 ∈ 𝐾 )
83 4 82 syl ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
84 83 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → 𝑌 ∈ 𝐾 )
85 txopn ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾 ) ) → ( 𝑢 × 𝑌 ) ∈ ( 𝐽 ×t 𝐾 ) )
86 79 80 81 84 85 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → ( 𝑢 × 𝑌 ) ∈ ( 𝐽 ×t 𝐾 ) )
87 eleq2 ⊢ ( 𝑤 = ( 𝑢 × 𝑌 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ↔ ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑌 ) ) )
88 eleq2 ⊢ ( 𝑤 = ( 𝑢 × 𝑌 ) → ( ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ↔ ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) ) )
89 88 rexralbidv ⊢ ( 𝑤 = ( 𝑢 × 𝑌 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) ) )
90 87 89 imbi12d ⊢ ( 𝑤 = ( 𝑢 × 𝑌 ) → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) ) ) )
91 90 rspcv ⊢ ( ( 𝑢 × 𝑌 ) ∈ ( 𝐽 ×t 𝐾 ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) ) ) )
92 86 91 syl ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) ) ) )
93 simprl ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → 𝑆 ∈ 𝑌 )
94 opelxpi ⊢ ( ( 𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑌 ) → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑌 ) )
95 93 94 sylan2 ⊢ ( ( 𝑅 ∈ 𝑢 ∧ ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) ) → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑌 ) )
96 95 expcom ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → ( 𝑅 ∈ 𝑢 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑌 ) ) )
97 53 eleq1d ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) ↔ ⟨ ( 𝐹 ‘ 𝑘 ) , ( 𝐺 ‘ 𝑘 ) ⟩ ∈ ( 𝑢 × 𝑌 ) ) )
98 opelxp1 ⊢ ( ⟨ ( 𝐹 ‘ 𝑘 ) , ( 𝐺 ‘ 𝑘 ) ⟩ ∈ ( 𝑢 × 𝑌 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 )
99 97 98 biimtrdi ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
100 47 99 syl ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
101 100 ralimdva ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
102 101 reximia ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 )
103 102 a1i ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
104 96 103 imim12d ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑢 × 𝑌 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑢 × 𝑌 ) ) → ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
105 92 104 syld ⊢ ( ( 𝜑 ∧ ( 𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽 ) ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
106 105 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝑌 ) ∧ 𝑢 ∈ 𝐽 ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
107 106 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑌 ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
108 107 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
109 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → 𝐽 ∈ Top )
110 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → 𝐾 ∈ Top )
111 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
112 3 111 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
113 112 adantr ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → 𝑋 ∈ 𝐽 )
114 simprr ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → 𝑣 ∈ 𝐾 )
115 txopn ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑋 ∈ 𝐽 ∧ 𝑣 ∈ 𝐾 ) ) → ( 𝑋 × 𝑣 ) ∈ ( 𝐽 ×t 𝐾 ) )
116 109 110 113 114 115 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → ( 𝑋 × 𝑣 ) ∈ ( 𝐽 ×t 𝐾 ) )
117 eleq2 ⊢ ( 𝑤 = ( 𝑋 × 𝑣 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 ↔ ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑣 ) ) )
118 eleq2 ⊢ ( 𝑤 = ( 𝑋 × 𝑣 ) → ( ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ↔ ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) ) )
119 118 rexralbidv ⊢ ( 𝑤 = ( 𝑋 × 𝑣 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) ) )
120 117 119 imbi12d ⊢ ( 𝑤 = ( 𝑋 × 𝑣 ) → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑣 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) ) ) )
121 120 rspcv ⊢ ( ( 𝑋 × 𝑣 ) ∈ ( 𝐽 ×t 𝐾 ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑣 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) ) ) )
122 116 121 syl ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑣 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) ) ) )
123 opelxpi ⊢ ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑣 ) → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑣 ) )
124 123 ex ⊢ ( 𝑅 ∈ 𝑋 → ( 𝑆 ∈ 𝑣 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑣 ) ) )
125 124 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → ( 𝑆 ∈ 𝑣 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑣 ) ) )
126 53 eleq1d ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) ↔ ⟨ ( 𝐹 ‘ 𝑘 ) , ( 𝐺 ‘ 𝑘 ) ⟩ ∈ ( 𝑋 × 𝑣 ) ) )
127 opelxp2 ⊢ ( ⟨ ( 𝐹 ‘ 𝑘 ) , ( 𝐺 ‘ 𝑘 ) ⟩ ∈ ( 𝑋 × 𝑣 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 )
128 126 127 biimtrdi ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) )
129 47 128 syl ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) )
130 129 ralimdva ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) )
131 130 reximia ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 )
132 131 a1i ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) )
133 125 132 imim12d ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑣 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ ( 𝑋 × 𝑣 ) ) → ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
134 122 133 syld ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾 ) ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
135 134 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝐾 ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
136 135 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝑋 ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
137 136 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) )
138 108 137 jcad ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ) → ( ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ) )
139 78 138 impbid ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ) → ( ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ↔ ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
140 139 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ∧ ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ) ↔ ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ∧ ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) ) )
141 opelxp ⊢ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) )
142 141 anbi1i ⊢ ( ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) ↔ ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ∧ ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) )
143 140 142 bitr4di ⊢ ( 𝜑 → ( ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ∧ ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) ) )
144 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
145 3 1 2 5 144 lmbrf ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑅 ↔ ( 𝑅 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
146 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
147 4 1 2 6 146 lmbrf ⊢ ( 𝜑 → ( 𝐺 ( ⇝𝑡 ‘ 𝐾 ) 𝑆 ↔ ( 𝑆 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ) )
148 145 147 anbi12d ⊢ ( 𝜑 → ( ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑅 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐾 ) 𝑆 ) ↔ ( ( 𝑅 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ∧ ( 𝑆 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ) ) )
149 an4 ⊢ ( ( ( 𝑅 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ∧ ( 𝑆 ∈ 𝑌 ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ) ↔ ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ∧ ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ) )
150 148 149 bitrdi ⊢ ( 𝜑 → ( ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑅 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐾 ) 𝑆 ) ↔ ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) ∧ ( ∀ 𝑢 ∈ 𝐽 ( 𝑅 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ∧ ∀ 𝑣 ∈ 𝐾 ( 𝑆 ∈ 𝑣 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ 𝑣 ) ) ) ) )
151 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
152 3 4 151 syl2anc ⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
153 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 )
154 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑛 ) ∈ 𝑌 )
155 153 154 opelxpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
156 155 7 fmptd ⊢ ( 𝜑 → 𝐻 : 𝑍 ⟶ ( 𝑋 × 𝑌 ) )
157 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐻 ‘ 𝑘 ) )
158 152 1 2 156 157 lmbrf ⊢ ( 𝜑 → ( 𝐻 ( ⇝𝑡 ‘ ( 𝐽 ×t 𝐾 ) ) ⟨ 𝑅 , 𝑆 ⟩ ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ∀ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝑅 , 𝑆 ⟩ ∈ 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐻 ‘ 𝑘 ) ∈ 𝑤 ) ) ) )
159 143 150 158 3bitr4d ⊢ ( 𝜑 → ( ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑅 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐾 ) 𝑆 ) ↔ 𝐻 ( ⇝𝑡 ‘ ( 𝐽 ×t 𝐾 ) ) ⟨ 𝑅 , 𝑆 ⟩ ) )