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

Theorem tx1stc 22252
 Description: The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
tx1stc ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ 1stω)

Proof of Theorem tx1stc
Dummy variables 𝑎 𝑏 𝑚 𝑛 𝑝 𝑞 𝑟 𝑠 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1stctop 22045 . . 3 (𝑅 ∈ 1stω → 𝑅 ∈ Top)
2 1stctop 22045 . . 3 (𝑆 ∈ 1stω → 𝑆 ∈ Top)
3 txtop 22171 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
41, 2, 3syl2an 597 . 2 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ Top)
5 eqid 2821 . . . . . . . 8 𝑅 = 𝑅
651stcclb 22046 . . . . . . 7 ((𝑅 ∈ 1stω ∧ 𝑢 𝑅) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))))
76ad2ant2r 745 . . . . . 6 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))))
8 eqid 2821 . . . . . . . 8 𝑆 = 𝑆
981stcclb 22046 . . . . . . 7 ((𝑆 ∈ 1stω ∧ 𝑣 𝑆) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
109ad2ant2l 744 . . . . . 6 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
11 reeanv 3367 . . . . . . 7 (∃𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))))
12 an4 654 . . . . . . . . 9 (((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))))
13 txopn 22204 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚𝑅𝑛𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
1413ralrimivva 3191 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
151, 2, 14syl2an 597 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
1615adantr 483 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
17 elpwi 4550 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ 𝒫 𝑅𝑎𝑅)
18 ssralv 4032 . . . . . . . . . . . . . . . . . 18 (𝑎𝑅 → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
1917, 18syl 17 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ 𝒫 𝑅 → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
20 elpwi 4550 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ 𝒫 𝑆𝑏𝑆)
21 ssralv 4032 . . . . . . . . . . . . . . . . . . 19 (𝑏𝑆 → (∀𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2220, 21syl 17 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 𝑆 → (∀𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2322ralimdv 3178 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ 𝒫 𝑆 → (∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2419, 23sylan9 510 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆) → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2516, 24mpan9 509 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
26 eqid 2821 . . . . . . . . . . . . . . . 16 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) = (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))
2726fmpo 7760 . . . . . . . . . . . . . . 15 (∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
2825, 27sylib 220 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
2928frnd 6515 . . . . . . . . . . . . 13 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
30 ovex 7183 . . . . . . . . . . . . . 14 (𝑅 ×t 𝑆) ∈ V
3130elpw2 5240 . . . . . . . . . . . . 13 (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
3229, 31sylibr 236 . . . . . . . . . . . 12 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
3332adantr 483 . . . . . . . . . . 11 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
34 omelon 9103 . . . . . . . . . . . . . . 15 ω ∈ On
35 xpct 9436 . . . . . . . . . . . . . . 15 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω)
36 ondomen 9457 . . . . . . . . . . . . . . 15 ((ω ∈ On ∧ (𝑎 × 𝑏) ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
3734, 35, 36sylancr 589 . . . . . . . . . . . . . 14 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
38 vex 3497 . . . . . . . . . . . . . . . . 17 𝑚 ∈ V
39 vex 3497 . . . . . . . . . . . . . . . . 17 𝑛 ∈ V
4038, 39xpex 7470 . . . . . . . . . . . . . . . 16 (𝑚 × 𝑛) ∈ V
4126, 40fnmpoi 7762 . . . . . . . . . . . . . . 15 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏)
42 dffn4 6590 . . . . . . . . . . . . . . 15 ((𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)))
4341, 42mpbi 232 . . . . . . . . . . . . . 14 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))
44 fodomnum 9477 . . . . . . . . . . . . . 14 ((𝑎 × 𝑏) ∈ dom card → ((𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)))
4537, 43, 44mpisyl 21 . . . . . . . . . . . . 13 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))
46 domtr 8556 . . . . . . . . . . . . 13 ((ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
4745, 35, 46syl2anc 586 . . . . . . . . . . . 12 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
4847ad2antrl 726 . . . . . . . . . . 11 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
491, 2anim12i 614 . . . . . . . . . . . . . . 15 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
5049ad3antrrr 728 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
51 eltx 22170 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
5250, 51syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
53 eleq1 2900 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨𝑢, 𝑣⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠)))
5453anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
55542rexbidv 3300 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑢, 𝑣⟩ → (∃𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
5655rspccv 3619 . . . . . . . . . . . . . 14 (∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
57 r19.27v 3184 . . . . . . . . . . . . . . . . . 18 ((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → ∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
58 r19.29 3254 . . . . . . . . . . . . . . . . . . 19 ((∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅 (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
59 r19.29 3254 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
60 opelxp 5585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ↔ (𝑢𝑟𝑣𝑠))
61 pm3.35 801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑟 ∧ (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))
62 pm3.35 801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣𝑠 ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))
6361, 62anim12i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑢𝑟 ∧ (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑣𝑠 ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
6463an4s 658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑢𝑟𝑣𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
6560, 64sylanb 583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
6665anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
6766anasss 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
6867an12s 647 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
6968expl 460 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → (((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
7069reximdv 3273 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → (∃𝑠𝑆 ((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
7159, 70syl5 34 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → ((∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
7271impl 458 . . . . . . . . . . . . . . . . . . . 20 ((((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7372reximi 3243 . . . . . . . . . . . . . . . . . . 19 (∃𝑟𝑅 (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7458, 73syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7557, 74sylan 582 . . . . . . . . . . . . . . . . 17 (((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
76 reeanv 3367 . . . . . . . . . . . . . . . . . . . 20 (∃𝑝𝑎𝑞𝑏 ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ↔ (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
77 simpr1l 1226 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝𝑎)
78 simpr1r 1227 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞𝑏)
79 eqidd 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞))
80 xpeq1 5563 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛))
8180eqeq2d 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛)))
82 xpeq2 5570 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞))
8382eqeq2d 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞)))
8481, 83rspc2ev 3634 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑎𝑞𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
8577, 78, 79, 84syl3anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
86 vex 3497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑝 ∈ V
87 vex 3497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑞 ∈ V
8886, 87xpex 7470 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 × 𝑞) ∈ V
89 eqeq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛)))
90892rexbidv 3300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑝 × 𝑞) → (∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)))
9188, 90elab 3666 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
9285, 91sylibr 236 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)})
9326rnmpo 7278 . . . . . . . . . . . . . . . . . . . . . . . 24 ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)}
9492, 93eleqtrrdi 2924 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)))
95 simpr2 1191 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)))
96 opelxpi 5586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢𝑝𝑣𝑞) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
9796ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
9895, 97syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
99 xpss12 5564 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑟𝑞𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
10099ad2ant2l 744 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
10195, 100syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
102 simpr3 1192 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧)
103101, 102sstrd 3976 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧)
104 eleq2 2901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑝 × 𝑞) → (⟨𝑢, 𝑣⟩ ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞)))
105 sseq1 3991 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑝 × 𝑞) → (𝑤𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧))
106104, 105anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑝 × 𝑞) → ((⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)))
107106rspcev 3622 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑝 × 𝑞) ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))
10894, 98, 103, 107syl12anc 834 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))
1091083exp2 1350 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → ((𝑝𝑎𝑞𝑏) → (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
110109rexlimdvv 3293 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → (∃𝑝𝑎𝑞𝑏 ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
11176, 110syl5bir 245 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
112111impd 413 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → (((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
113112rexlimdvva 3294 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
11475, 113syl5 34 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
115114expd 418 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → (∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
116115impr 457 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
11756, 116syl9r 78 . . . . . . . . . . . . 13 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
11852, 117sylbid 242 . . . . . . . . . . . 12 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
119118ralrimiv 3181 . . . . . . . . . . 11 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
120 breq1 5061 . . . . . . . . . . . . 13 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω))
121 rexeq 3406 . . . . . . . . . . . . . . 15 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧) ↔ ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
122121imbi2d 343 . . . . . . . . . . . . . 14 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ((⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
123122ralbidv 3197 . . . . . . . . . . . . 13 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
124120, 123anbi12d 632 . . . . . . . . . . . 12 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))) ↔ (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
125124rspcev 3622 . . . . . . . . . . 11 ((ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
12633, 48, 119, 125syl12anc 834 . . . . . . . . . 10 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
127126ex 415 . . . . . . . . 9 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
12812, 127syl5bi 244 . . . . . . . 8 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
129128rexlimdvva 3294 . . . . . . 7 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
13011, 129syl5bir 245 . . . . . 6 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
1317, 10, 130mp2and 697 . . . . 5 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
132131ralrimivva 3191 . . . 4 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑢 𝑅𝑣 𝑆𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
133 eleq1 2900 . . . . . . . . 9 (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥𝑧 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑧))
134 eleq1 2900 . . . . . . . . . . 11 (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑤))
135134anbi1d 631 . . . . . . . . . 10 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑤𝑤𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
136135rexbidv 3297 . . . . . . . . 9 (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑤𝑦 (𝑥𝑤𝑤𝑧) ↔ ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
137133, 136imbi12d 347 . . . . . . . 8 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
138137ralbidv 3197 . . . . . . 7 (𝑥 = ⟨𝑢, 𝑣⟩ → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
139138anbi2d 630 . . . . . 6 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
140139rexbidv 3297 . . . . 5 (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
141140ralxp 5706 . . . 4 (∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∀𝑢 𝑅𝑣 𝑆𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
142132, 141sylibr 236 . . 3 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
1435, 8txuni 22194 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1441, 2, 143syl2an 597 . . . 4 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
145144raleqdv 3415 . . 3 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)))))
146142, 145mpbid 234 . 2 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
147 eqid 2821 . . 3 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
148147is1stc2 22044 . 2 ((𝑅 ×t 𝑆) ∈ 1stω ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)))))
1494, 146, 148sylanbrc 585 1 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ 1stω)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  {cab 2799  ∀wral 3138  ∃wrex 3139   ⊆ wss 3935  𝒫 cpw 4538  ⟨cop 4566  ∪ cuni 4831   class class class wbr 5058   × cxp 5547  dom cdm 5549  ran crn 5550  Oncon0 6185   Fn wfn 6344  ⟶wf 6345  –onto→wfo 6347  (class class class)co 7150   ∈ cmpo 7152  ωcom 7574   ≼ cdom 8501  cardccrd 9358  Topctop 21495  1stωc1stc 22039   ×t ctx 22162 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-inf2 9098 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-oi 8968  df-card 9362  df-acn 9365  df-topgen 16711  df-top 21496  df-topon 21513  df-bases 21548  df-1stc 22041  df-tx 22164 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator