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

Theorem tx1stc 21663
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 21456 . . 3 (𝑅 ∈ 1st𝜔 → 𝑅 ∈ Top)
2 1stctop 21456 . . 3 (𝑆 ∈ 1st𝜔 → 𝑆 ∈ Top)
3 txtop 21582 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
41, 2, 3syl2an 585 . 2 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ×t 𝑆) ∈ Top)
5 eqid 2805 . . . . . . . 8 𝑅 = 𝑅
651stcclb 21457 . . . . . . 7 ((𝑅 ∈ 1st𝜔 ∧ 𝑢 𝑅) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))))
76ad2ant2r 744 . . . . . 6 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))))
8 eqid 2805 . . . . . . . 8 𝑆 = 𝑆
981stcclb 21457 . . . . . . 7 ((𝑆 ∈ 1st𝜔 ∧ 𝑣 𝑆) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
109ad2ant2l 743 . . . . . 6 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
11 reeanv 3294 . . . . . . 7 (∃𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))))
12 an4 638 . . . . . . . . 9 (((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))))
13 txopn 21615 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚𝑅𝑛𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
1413ralrimivva 3158 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
151, 2, 14syl2an 585 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
1615adantr 468 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
17 elpwi 4358 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ 𝒫 𝑅𝑎𝑅)
18 ssralv 3860 . . . . . . . . . . . . . . . . . 18 (𝑎𝑅 → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
1917, 18syl 17 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ 𝒫 𝑅 → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
20 elpwi 4358 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ 𝒫 𝑆𝑏𝑆)
21 ssralv 3860 . . . . . . . . . . . . . . . . . . 19 (𝑏𝑆 → (∀𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2220, 21syl 17 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 𝑆 → (∀𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2322ralimdv 3150 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ 𝒫 𝑆 → (∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2419, 23sylan9 499 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆) → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2516, 24mpan9 498 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
26 eqid 2805 . . . . . . . . . . . . . . . 16 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) = (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))
2726fmpt2 7467 . . . . . . . . . . . . . . 15 (∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
2825, 27sylib 209 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
2928frnd 6260 . . . . . . . . . . . . 13 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
30 ovex 6903 . . . . . . . . . . . . . 14 (𝑅 ×t 𝑆) ∈ V
3130elpw2 5017 . . . . . . . . . . . . 13 (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
3229, 31sylibr 225 . . . . . . . . . . . 12 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
3332adantr 468 . . . . . . . . . . 11 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
34 omelon 8787 . . . . . . . . . . . . . . 15 ω ∈ On
35 vex 3393 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ V
3635xpdom1 8295 . . . . . . . . . . . . . . . . 17 (𝑎 ≼ ω → (𝑎 × 𝑏) ≼ (ω × 𝑏))
37 omex 8784 . . . . . . . . . . . . . . . . . 18 ω ∈ V
3837xpdom2 8291 . . . . . . . . . . . . . . . . 17 (𝑏 ≼ ω → (ω × 𝑏) ≼ (ω × ω))
39 domtr 8242 . . . . . . . . . . . . . . . . 17 (((𝑎 × 𝑏) ≼ (ω × 𝑏) ∧ (ω × 𝑏) ≼ (ω × ω)) → (𝑎 × 𝑏) ≼ (ω × ω))
4036, 38, 39syl2an 585 . . . . . . . . . . . . . . . 16 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ (ω × ω))
41 xpomen 9118 . . . . . . . . . . . . . . . 16 (ω × ω) ≈ ω
42 domentr 8248 . . . . . . . . . . . . . . . 16 (((𝑎 × 𝑏) ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → (𝑎 × 𝑏) ≼ ω)
4340, 41, 42sylancl 576 . . . . . . . . . . . . . . 15 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω)
44 ondomen 9140 . . . . . . . . . . . . . . 15 ((ω ∈ On ∧ (𝑎 × 𝑏) ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
4534, 43, 44sylancr 577 . . . . . . . . . . . . . 14 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
46 vex 3393 . . . . . . . . . . . . . . . . 17 𝑚 ∈ V
47 vex 3393 . . . . . . . . . . . . . . . . 17 𝑛 ∈ V
4846, 47xpex 7189 . . . . . . . . . . . . . . . 16 (𝑚 × 𝑛) ∈ V
4926, 48fnmpt2i 7469 . . . . . . . . . . . . . . 15 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏)
50 dffn4 6334 . . . . . . . . . . . . . . 15 ((𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)))
5149, 50mpbi 221 . . . . . . . . . . . . . 14 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))
52 fodomnum 9160 . . . . . . . . . . . . . 14 ((𝑎 × 𝑏) ∈ dom card → ((𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)))
5345, 51, 52mpisyl 21 . . . . . . . . . . . . 13 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))
54 domtr 8242 . . . . . . . . . . . . 13 ((ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
5553, 43, 54syl2anc 575 . . . . . . . . . . . 12 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
5655ad2antrl 710 . . . . . . . . . . 11 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
571, 2anim12i 602 . . . . . . . . . . . . . . 15 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
5857ad3antrrr 712 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
59 eltx 21581 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
6058, 59syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
61 eleq1 2872 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨𝑢, 𝑣⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠)))
6261anbi1d 617 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
63622rexbidv 3244 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑢, 𝑣⟩ → (∃𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
6463rspccv 3498 . . . . . . . . . . . . . 14 (∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
65 r19.27v 3257 . . . . . . . . . . . . . . . . . 18 ((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → ∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
66 r19.29 3259 . . . . . . . . . . . . . . . . . . 19 ((∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅 (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
67 r19.29 3259 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
68 opelxp 5343 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ↔ (𝑢𝑟𝑣𝑠))
69 pm3.35 828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑟 ∧ (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))
70 pm3.35 828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣𝑠 ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))
7169, 70anim12i 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑢𝑟 ∧ (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑣𝑠 ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
7271an4s 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑢𝑟𝑣𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
7368, 72sylanb 572 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
7473anim1i 604 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7574anasss 454 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7675an12s 631 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7776expl 447 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → (((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
7877reximdv 3202 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → (∃𝑠𝑆 ((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
7967, 78syl5 34 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → ((∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
8079impl 445 . . . . . . . . . . . . . . . . . . . 20 ((((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
8180reximi 3197 . . . . . . . . . . . . . . . . . . 19 (∃𝑟𝑅 (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
8266, 81syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
8365, 82sylan 571 . . . . . . . . . . . . . . . . 17 (((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
84 reeanv 3294 . . . . . . . . . . . . . . . . . . . 20 (∃𝑝𝑎𝑞𝑏 ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ↔ (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
85 simpr1l 1298 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝𝑎)
86 simpr1r 1300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞𝑏)
87 eqidd 2806 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞))
88 xpeq1 5322 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛))
8988eqeq2d 2815 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛)))
90 xpeq2 5328 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞))
9190eqeq2d 2815 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞)))
9289, 91rspc2ev 3516 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑎𝑞𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
9385, 86, 87, 92syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
94 vex 3393 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑝 ∈ V
95 vex 3393 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑞 ∈ V
9694, 95xpex 7189 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 × 𝑞) ∈ V
97 eqeq1 2809 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛)))
98972rexbidv 3244 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑝 × 𝑞) → (∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)))
9996, 98elab 3544 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
10093, 99sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)})
10126rnmpt2 6997 . . . . . . . . . . . . . . . . . . . . . . . 24 ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)}
102100, 101syl6eleqr 2895 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)))
103 simpr2 1243 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)))
104 opelxpi 5345 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢𝑝𝑣𝑞) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
105104ad2ant2r 744 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
106103, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
107 xpss12 5323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑟𝑞𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
108107ad2ant2l 743 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
109103, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
110 simpr3 1245 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧)
111109, 110sstrd 3805 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧)
112 eleq2 2873 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑝 × 𝑞) → (⟨𝑢, 𝑣⟩ ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞)))
113 sseq1 3820 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑝 × 𝑞) → (𝑤𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧))
114112, 113anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑝 × 𝑞) → ((⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)))
115114rspcev 3501 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑝 × 𝑞) ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))
116102, 106, 111, 115syl12anc 856 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))
1171163exp2 1456 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → ((𝑝𝑎𝑞𝑏) → (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
118117rexlimdvv 3224 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → (∃𝑝𝑎𝑞𝑏 ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
11984, 118syl5bir 234 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
120119impd 398 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → (((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
121120rexlimdvva 3225 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
12283, 121syl5 34 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
123122expd 402 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → (∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
124123impr 444 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
12564, 124syl9r 78 . . . . . . . . . . . . 13 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
12660, 125sylbid 231 . . . . . . . . . . . 12 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
127126ralrimiv 3152 . . . . . . . . . . 11 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
128 breq1 4843 . . . . . . . . . . . . 13 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω))
129 rexeq 3327 . . . . . . . . . . . . . . 15 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧) ↔ ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
130129imbi2d 331 . . . . . . . . . . . . . 14 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ((⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
131130ralbidv 3173 . . . . . . . . . . . . 13 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
132128, 131anbi12d 618 . . . . . . . . . . . 12 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))) ↔ (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
133132rspcev 3501 . . . . . . . . . . 11 ((ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
13433, 56, 127, 133syl12anc 856 . . . . . . . . . 10 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
135134ex 399 . . . . . . . . 9 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
13612, 135syl5bi 233 . . . . . . . 8 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
137136rexlimdvva 3225 . . . . . . 7 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
13811, 137syl5bir 234 . . . . . 6 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
1397, 10, 138mp2and 682 . . . . 5 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
140139ralrimivva 3158 . . . 4 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑢 𝑅𝑣 𝑆𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
141 eleq1 2872 . . . . . . . . 9 (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥𝑧 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑧))
142 eleq1 2872 . . . . . . . . . . 11 (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑤))
143142anbi1d 617 . . . . . . . . . 10 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑤𝑤𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
144143rexbidv 3239 . . . . . . . . 9 (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑤𝑦 (𝑥𝑤𝑤𝑧) ↔ ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
145141, 144imbi12d 335 . . . . . . . 8 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
146145ralbidv 3173 . . . . . . 7 (𝑥 = ⟨𝑢, 𝑣⟩ → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
147146anbi2d 616 . . . . . 6 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
148147rexbidv 3239 . . . . 5 (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
149148ralxp 5462 . . . 4 (∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∀𝑢 𝑅𝑣 𝑆𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
150140, 149sylibr 225 . . 3 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
1515, 8txuni 21605 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1521, 2, 151syl2an 585 . . . 4 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
153152raleqdv 3332 . . 3 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)))))
154150, 153mpbid 223 . 2 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
155 eqid 2805 . . 3 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
156155is1stc2 21455 . 2 ((𝑅 ×t 𝑆) ∈ 1st𝜔 ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)))))
1574, 154, 156sylanbrc 574 1 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ×t 𝑆) ∈ 1st𝜔)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2158  {cab 2791  wral 3095  wrex 3096  wss 3766  𝒫 cpw 4348  cop 4373   cuni 4626   class class class wbr 4840   × cxp 5306  dom cdm 5308  ran crn 5309  Oncon0 5933   Fn wfn 6093  wf 6094  ontowfo 6096  (class class class)co 6871  cmpt2 6873  ωcom 7292  cen 8186  cdom 8187  cardccrd 9041  Topctop 20907  1st𝜔c1stc 21450   ×t ctx 21573
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-inf2 8782
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-1st 7395  df-2nd 7396  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-oadd 7797  df-er 7976  df-map 8091  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-oi 8651  df-card 9045  df-acn 9048  df-topgen 16305  df-top 20908  df-topon 20925  df-bases 20960  df-1stc 21452  df-tx 21575
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator