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

Theorem tx1stc 22186
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 21979 . . 3 (𝑅 ∈ 1stω → 𝑅 ∈ Top)
2 1stctop 21979 . . 3 (𝑆 ∈ 1stω → 𝑆 ∈ Top)
3 txtop 22105 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
41, 2, 3syl2an 595 . 2 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ Top)
5 eqid 2818 . . . . . . . 8 𝑅 = 𝑅
651stcclb 21980 . . . . . . 7 ((𝑅 ∈ 1stω ∧ 𝑢 𝑅) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))))
76ad2ant2r 743 . . . . . 6 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))))
8 eqid 2818 . . . . . . . 8 𝑆 = 𝑆
981stcclb 21980 . . . . . . 7 ((𝑆 ∈ 1stω ∧ 𝑣 𝑆) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
109ad2ant2l 742 . . . . . 6 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
11 reeanv 3365 . . . . . . 7 (∃𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))))
12 an4 652 . . . . . . . . 9 (((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))))
13 txopn 22138 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚𝑅𝑛𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
1413ralrimivva 3188 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
151, 2, 14syl2an 595 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
1615adantr 481 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
17 elpwi 4547 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ 𝒫 𝑅𝑎𝑅)
18 ssralv 4030 . . . . . . . . . . . . . . . . . 18 (𝑎𝑅 → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
1917, 18syl 17 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ 𝒫 𝑅 → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
20 elpwi 4547 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ 𝒫 𝑆𝑏𝑆)
21 ssralv 4030 . . . . . . . . . . . . . . . . . . 19 (𝑏𝑆 → (∀𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2220, 21syl 17 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 𝑆 → (∀𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2322ralimdv 3175 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ 𝒫 𝑆 → (∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2419, 23sylan9 508 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆) → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2516, 24mpan9 507 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
26 eqid 2818 . . . . . . . . . . . . . . . 16 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) = (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))
2726fmpo 7755 . . . . . . . . . . . . . . 15 (∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
2825, 27sylib 219 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
2928frnd 6514 . . . . . . . . . . . . 13 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
30 ovex 7178 . . . . . . . . . . . . . 14 (𝑅 ×t 𝑆) ∈ V
3130elpw2 5239 . . . . . . . . . . . . 13 (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
3229, 31sylibr 235 . . . . . . . . . . . 12 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
3332adantr 481 . . . . . . . . . . 11 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
34 omelon 9097 . . . . . . . . . . . . . . 15 ω ∈ On
35 xpct 9430 . . . . . . . . . . . . . . 15 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω)
36 ondomen 9451 . . . . . . . . . . . . . . 15 ((ω ∈ On ∧ (𝑎 × 𝑏) ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
3734, 35, 36sylancr 587 . . . . . . . . . . . . . 14 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
38 vex 3495 . . . . . . . . . . . . . . . . 17 𝑚 ∈ V
39 vex 3495 . . . . . . . . . . . . . . . . 17 𝑛 ∈ V
4038, 39xpex 7465 . . . . . . . . . . . . . . . 16 (𝑚 × 𝑛) ∈ V
4126, 40fnmpoi 7757 . . . . . . . . . . . . . . 15 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏)
42 dffn4 6589 . . . . . . . . . . . . . . 15 ((𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)))
4341, 42mpbi 231 . . . . . . . . . . . . . 14 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))
44 fodomnum 9471 . . . . . . . . . . . . . 14 ((𝑎 × 𝑏) ∈ dom card → ((𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)))
4537, 43, 44mpisyl 21 . . . . . . . . . . . . 13 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))
46 domtr 8550 . . . . . . . . . . . . 13 ((ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
4745, 35, 46syl2anc 584 . . . . . . . . . . . 12 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
4847ad2antrl 724 . . . . . . . . . . 11 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
491, 2anim12i 612 . . . . . . . . . . . . . . 15 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
5049ad3antrrr 726 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
51 eltx 22104 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
5250, 51syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
53 eleq1 2897 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨𝑢, 𝑣⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠)))
5453anbi1d 629 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
55542rexbidv 3297 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑢, 𝑣⟩ → (∃𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
5655rspccv 3617 . . . . . . . . . . . . . 14 (∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
57 r19.27v 3181 . . . . . . . . . . . . . . . . . 18 ((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → ∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
58 r19.29 3251 . . . . . . . . . . . . . . . . . . 19 ((∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅 (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
59 r19.29 3251 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
60 opelxp 5584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ↔ (𝑢𝑟𝑣𝑠))
61 pm3.35 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑟 ∧ (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))
62 pm3.35 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣𝑠 ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))
6361, 62anim12i 612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑢𝑟 ∧ (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑣𝑠 ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
6463an4s 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑢𝑟𝑣𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
6560, 64sylanb 581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
6665anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
6766anasss 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
6867an12s 645 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
6968expl 458 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → (((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
7069reximdv 3270 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → (∃𝑠𝑆 ((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
7159, 70syl5 34 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → ((∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
7271impl 456 . . . . . . . . . . . . . . . . . . . 20 ((((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7372reximi 3240 . . . . . . . . . . . . . . . . . . 19 (∃𝑟𝑅 (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7458, 73syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7557, 74sylan 580 . . . . . . . . . . . . . . . . 17 (((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
76 reeanv 3365 . . . . . . . . . . . . . . . . . . . 20 (∃𝑝𝑎𝑞𝑏 ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ↔ (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
77 simpr1l 1222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝𝑎)
78 simpr1r 1223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞𝑏)
79 eqidd 2819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞))
80 xpeq1 5562 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛))
8180eqeq2d 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛)))
82 xpeq2 5569 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞))
8382eqeq2d 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞)))
8481, 83rspc2ev 3632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑎𝑞𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
8577, 78, 79, 84syl3anc 1363 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
86 vex 3495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑝 ∈ V
87 vex 3495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑞 ∈ V
8886, 87xpex 7465 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 × 𝑞) ∈ V
89 eqeq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛)))
90892rexbidv 3297 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑝 × 𝑞) → (∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)))
9188, 90elab 3664 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
9285, 91sylibr 235 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)})
9326rnmpo 7273 . . . . . . . . . . . . . . . . . . . . . . . 24 ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)}
9492, 93eleqtrrdi 2921 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)))
95 simpr2 1187 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)))
96 opelxpi 5585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢𝑝𝑣𝑞) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
9796ad2ant2r 743 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
9895, 97syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
99 xpss12 5563 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑟𝑞𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
10099ad2ant2l 742 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
10195, 100syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
102 simpr3 1188 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧)
103101, 102sstrd 3974 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧)
104 eleq2 2898 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑝 × 𝑞) → (⟨𝑢, 𝑣⟩ ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞)))
105 sseq1 3989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑝 × 𝑞) → (𝑤𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧))
106104, 105anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑝 × 𝑞) → ((⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)))
107106rspcev 3620 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑝 × 𝑞) ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))
10894, 98, 103, 107syl12anc 832 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))
1091083exp2 1346 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → ((𝑝𝑎𝑞𝑏) → (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
110109rexlimdvv 3290 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → (∃𝑝𝑎𝑞𝑏 ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
11176, 110syl5bir 244 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
112111impd 411 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → (((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
113112rexlimdvva 3291 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
11475, 113syl5 34 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
115114expd 416 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → (∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
116115impr 455 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
11756, 116syl9r 78 . . . . . . . . . . . . 13 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
11852, 117sylbid 241 . . . . . . . . . . . 12 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
119118ralrimiv 3178 . . . . . . . . . . 11 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
120 breq1 5060 . . . . . . . . . . . . 13 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω))
121 rexeq 3404 . . . . . . . . . . . . . . 15 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧) ↔ ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
122121imbi2d 342 . . . . . . . . . . . . . 14 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ((⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
123122ralbidv 3194 . . . . . . . . . . . . 13 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
124120, 123anbi12d 630 . . . . . . . . . . . 12 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))) ↔ (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
125124rspcev 3620 . . . . . . . . . . 11 ((ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
12633, 48, 119, 125syl12anc 832 . . . . . . . . . 10 (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
127126ex 413 . . . . . . . . 9 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
12812, 127syl5bi 243 . . . . . . . 8 ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
129128rexlimdvva 3291 . . . . . . 7 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
13011, 129syl5bir 244 . . . . . 6 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
1317, 10, 130mp2and 695 . . . . 5 (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
132131ralrimivva 3188 . . . 4 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑢 𝑅𝑣 𝑆𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
133 eleq1 2897 . . . . . . . . 9 (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥𝑧 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑧))
134 eleq1 2897 . . . . . . . . . . 11 (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑤))
135134anbi1d 629 . . . . . . . . . 10 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑤𝑤𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
136135rexbidv 3294 . . . . . . . . 9 (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑤𝑦 (𝑥𝑤𝑤𝑧) ↔ ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
137133, 136imbi12d 346 . . . . . . . 8 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
138137ralbidv 3194 . . . . . . 7 (𝑥 = ⟨𝑢, 𝑣⟩ → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
139138anbi2d 628 . . . . . 6 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
140139rexbidv 3294 . . . . 5 (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
141140ralxp 5705 . . . 4 (∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∀𝑢 𝑅𝑣 𝑆𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
142132, 141sylibr 235 . . 3 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
1435, 8txuni 22128 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1441, 2, 143syl2an 595 . . . 4 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
145144raleqdv 3413 . . 3 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)))))
146142, 145mpbid 233 . 2 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
147 eqid 2818 . . 3 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
148147is1stc2 21978 . 2 ((𝑅 ×t 𝑆) ∈ 1stω ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)))))
1494, 146, 148sylanbrc 583 1 ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ 1stω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  {cab 2796  wral 3135  wrex 3136  wss 3933  𝒫 cpw 4535  cop 4563   cuni 4830   class class class wbr 5057   × cxp 5546  dom cdm 5548  ran crn 5549  Oncon0 6184   Fn wfn 6343  wf 6344  ontowfo 6346  (class class class)co 7145  cmpo 7147  ωcom 7569  cdom 8495  cardccrd 9352  Topctop 21429  1stωc1stc 21973   ×t ctx 22096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-oi 8962  df-card 9356  df-acn 9359  df-topgen 16705  df-top 21430  df-topon 21447  df-bases 21482  df-1stc 21975  df-tx 22098
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator