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

Theorem tx1stc 21376
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 21169 . . 3 (𝑅 ∈ 1st𝜔 → 𝑅 ∈ Top)
2 1stctop 21169 . . 3 (𝑆 ∈ 1st𝜔 → 𝑆 ∈ Top)
3 txtop 21295 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
41, 2, 3syl2an 494 . 2 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ×t 𝑆) ∈ Top)
5 eqid 2621 . . . . . . . 8 𝑅 = 𝑅
651stcclb 21170 . . . . . . 7 ((𝑅 ∈ 1st𝜔 ∧ 𝑢 𝑅) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))))
76ad2ant2r 782 . . . . . 6 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))))
8 eqid 2621 . . . . . . . 8 𝑆 = 𝑆
981stcclb 21170 . . . . . . 7 ((𝑆 ∈ 1st𝜔 ∧ 𝑣 𝑆) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
109ad2ant2l 781 . . . . . 6 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
11 reeanv 3100 . . . . . . 7 (∃𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))))
12 an4 864 . . . . . . . . 9 (((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))))
13 txopn 21328 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚𝑅𝑛𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
1413ralrimivva 2966 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
151, 2, 14syl2an 494 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
1615adantr 481 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
17 elpwi 4145 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ 𝒫 𝑅𝑎𝑅)
18 ssralv 3650 . . . . . . . . . . . . . . . . . 18 (𝑎𝑅 → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
1917, 18syl 17 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ 𝒫 𝑅 → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
20 elpwi 4145 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ 𝒫 𝑆𝑏𝑆)
21 ssralv 3650 . . . . . . . . . . . . . . . . . . 19 (𝑏𝑆 → (∀𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2220, 21syl 17 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ 𝒫 𝑆 → (∀𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2322ralimdv 2958 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ 𝒫 𝑆 → (∀𝑚𝑎𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2419, 23sylan9 688 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆) → (∀𝑚𝑅𝑛𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
2516, 24mpan9 486 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
26 eqid 2621 . . . . . . . . . . . . . . . 16 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) = (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))
2726fmpt2 7189 . . . . . . . . . . . . . . 15 (∀𝑚𝑎𝑛𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
2825, 27sylib 208 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
29 frn 6015 . . . . . . . . . . . . . 14 ((𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
3028, 29syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
31 ovex 6638 . . . . . . . . . . . . . 14 (𝑅 ×t 𝑆) ∈ V
3231elpw2 4793 . . . . . . . . . . . . 13 (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
3330, 32sylibr 224 . . . . . . . . . . . 12 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
3433adantr 481 . . . . . . . . . . 11 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
35 omelon 8495 . . . . . . . . . . . . . . 15 ω ∈ On
36 vex 3192 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ V
3736xpdom1 8011 . . . . . . . . . . . . . . . . 17 (𝑎 ≼ ω → (𝑎 × 𝑏) ≼ (ω × 𝑏))
38 omex 8492 . . . . . . . . . . . . . . . . . 18 ω ∈ V
3938xpdom2 8007 . . . . . . . . . . . . . . . . 17 (𝑏 ≼ ω → (ω × 𝑏) ≼ (ω × ω))
40 domtr 7961 . . . . . . . . . . . . . . . . 17 (((𝑎 × 𝑏) ≼ (ω × 𝑏) ∧ (ω × 𝑏) ≼ (ω × ω)) → (𝑎 × 𝑏) ≼ (ω × ω))
4137, 39, 40syl2an 494 . . . . . . . . . . . . . . . 16 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ (ω × ω))
42 xpomen 8790 . . . . . . . . . . . . . . . 16 (ω × ω) ≈ ω
43 domentr 7967 . . . . . . . . . . . . . . . 16 (((𝑎 × 𝑏) ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → (𝑎 × 𝑏) ≼ ω)
4441, 42, 43sylancl 693 . . . . . . . . . . . . . . 15 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω)
45 ondomen 8812 . . . . . . . . . . . . . . 15 ((ω ∈ On ∧ (𝑎 × 𝑏) ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
4635, 44, 45sylancr 694 . . . . . . . . . . . . . 14 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
47 vex 3192 . . . . . . . . . . . . . . . . 17 𝑚 ∈ V
48 vex 3192 . . . . . . . . . . . . . . . . 17 𝑛 ∈ V
4947, 48xpex 6922 . . . . . . . . . . . . . . . 16 (𝑚 × 𝑛) ∈ V
5026, 49fnmpt2i 7191 . . . . . . . . . . . . . . 15 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏)
51 dffn4 6083 . . . . . . . . . . . . . . 15 ((𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)))
5250, 51mpbi 220 . . . . . . . . . . . . . 14 (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))
53 fodomnum 8832 . . . . . . . . . . . . . 14 ((𝑎 × 𝑏) ∈ dom card → ((𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)))
5446, 52, 53mpisyl 21 . . . . . . . . . . . . 13 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))
55 domtr 7961 . . . . . . . . . . . . 13 ((ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
5654, 44, 55syl2anc 692 . . . . . . . . . . . 12 ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
5756ad2antrl 763 . . . . . . . . . . 11 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
581, 2anim12i 589 . . . . . . . . . . . . . . 15 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
5958ad3antrrr 765 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
60 eltx 21294 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
6159, 60syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
62 eleq1 2686 . . . . . . . . . . . . . . . . 17 (𝑤 = ⟨𝑢, 𝑣⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠)))
6362anbi1d 740 . . . . . . . . . . . . . . . 16 (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
64632rexbidv 3051 . . . . . . . . . . . . . . 15 (𝑤 = ⟨𝑢, 𝑣⟩ → (∃𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
6564rspccv 3295 . . . . . . . . . . . . . 14 (∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
66 r19.27v 3064 . . . . . . . . . . . . . . . . . 18 ((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → ∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))
67 r19.29 3066 . . . . . . . . . . . . . . . . . . 19 ((∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅 (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
68 r19.29 3066 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
69 opelxp 5111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ↔ (𝑢𝑟𝑣𝑠))
70 pm3.35 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑟 ∧ (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))
71 pm3.35 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑣𝑠 ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))
7270, 71anim12i 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑢𝑟 ∧ (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑣𝑠 ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
7372an4s 868 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑢𝑟𝑣𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
7469, 73sylanb 489 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
7574anim1i 591 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7675anasss 678 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7776an12s 842 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
7877expl 647 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → (((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
7978reximdv 3011 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → (∃𝑠𝑆 ((𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
8068, 79syl5 34 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) → ((∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
8180impl 649 . . . . . . . . . . . . . . . . . . . 20 ((((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
8281reximi 3006 . . . . . . . . . . . . . . . . . . 19 (∃𝑟𝑅 (((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
8367, 82syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑟𝑅 ((𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
8466, 83sylan 488 . . . . . . . . . . . . . . . . 17 (((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
85 reeanv 3100 . . . . . . . . . . . . . . . . . . . 20 (∃𝑝𝑎𝑞𝑏 ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ↔ (∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))
86 simpr1l 1116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝𝑎)
87 simpr1r 1117 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞𝑏)
88 eqidd 2622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞))
89 xpeq1 5093 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛))
9089eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛)))
91 xpeq2 5094 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞))
9291eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞)))
9390, 92rspc2ev 3312 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑎𝑞𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
9486, 87, 88, 93syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
95 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑝 ∈ V
96 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑞 ∈ V
9795, 96xpex 6922 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 × 𝑞) ∈ V
98 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛)))
99982rexbidv 3051 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑝 × 𝑞) → (∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)))
10097, 99elab 3337 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚𝑎𝑛𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
10194, 100sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)})
10226rnmpt2 6730 . . . . . . . . . . . . . . . . . . . . . . . 24 ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚𝑎𝑛𝑏 𝑥 = (𝑚 × 𝑛)}
103101, 102syl6eleqr 2709 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)))
104 simpr2 1066 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)))
105 opelxpi 5113 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑢𝑝𝑣𝑞) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
106105ad2ant2r 782 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
107104, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
108 xpss12 5191 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑝𝑟𝑞𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
109108ad2ant2l 781 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
110104, 109syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
111 simpr3 1067 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧)
112110, 111sstrd 3597 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧)
113 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑝 × 𝑞) → (⟨𝑢, 𝑣⟩ ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞)))
114 sseq1 3610 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑝 × 𝑞) → (𝑤𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧))
115113, 114anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑝 × 𝑞) → ((⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)))
116115rspcev 3298 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑝 × 𝑞) ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))
117103, 107, 112, 116syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) ∧ ((𝑝𝑎𝑞𝑏) ∧ ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))
1181173exp2 1282 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → ((𝑝𝑎𝑞𝑏) → (((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
119118rexlimdvv 3031 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → (∃𝑝𝑎𝑞𝑏 ((𝑢𝑝𝑝𝑟) ∧ (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
12085, 119syl5bir 233 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
121120impd 447 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟𝑅𝑠𝑆)) → (((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
122121rexlimdvva 3032 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟𝑅𝑠𝑆 ((∃𝑝𝑎 (𝑢𝑝𝑝𝑟) ∧ ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
12384, 122syl5 34 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) ∧ ∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
124123expd 452 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))) → (∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
125124impr 648 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (∃𝑟𝑅𝑠𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
12665, 125syl9r 78 . . . . . . . . . . . . 13 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (∀𝑤𝑧𝑟𝑅𝑠𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
12761, 126sylbid 230 . . . . . . . . . . . 12 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
128127ralrimiv 2960 . . . . . . . . . . 11 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
129 breq1 4621 . . . . . . . . . . . . 13 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω))
130 rexeq 3131 . . . . . . . . . . . . . . 15 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧) ↔ ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
131130imbi2d 330 . . . . . . . . . . . . . 14 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ((⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
132131ralbidv 2981 . . . . . . . . . . . . 13 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
133129, 132anbi12d 746 . . . . . . . . . . . 12 (𝑦 = ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))) ↔ (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
134133rspcev 3298 . . . . . . . . . . 11 ((ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚𝑎, 𝑛𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
13534, 57, 128, 134syl12anc 1321 . . . . . . . . . 10 (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
136135ex 450 . . . . . . . . 9 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟)) ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
13712, 136syl5bi 232 . . . . . . . 8 ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
138137rexlimdvva 3032 . . . . . . 7 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
13911, 138syl5bir 233 . . . . . 6 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟𝑅 (𝑢𝑟 → ∃𝑝𝑎 (𝑢𝑝𝑝𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠𝑆 (𝑣𝑠 → ∃𝑞𝑏 (𝑣𝑞𝑞𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
1407, 10, 139mp2and 714 . . . . 5 (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 𝑅𝑣 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
141140ralrimivva 2966 . . . 4 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑢 𝑅𝑣 𝑆𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
142 eleq1 2686 . . . . . . . . 9 (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥𝑧 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑧))
143 eleq1 2686 . . . . . . . . . . 11 (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑤))
144143anbi1d 740 . . . . . . . . . 10 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑤𝑤𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
145144rexbidv 3046 . . . . . . . . 9 (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑤𝑦 (𝑥𝑤𝑤𝑧) ↔ ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))
146142, 145imbi12d 334 . . . . . . . 8 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
147146ralbidv 2981 . . . . . . 7 (𝑥 = ⟨𝑢, 𝑣⟩ → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
148147anbi2d 739 . . . . . 6 (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
149148rexbidv 3046 . . . . 5 (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧)))))
150149ralxp 5228 . . . 4 (∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∀𝑢 𝑅𝑣 𝑆𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤𝑤𝑧))))
151141, 150sylibr 224 . . 3 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
1525, 8txuni 21318 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1531, 2, 152syl2an 494 . . . 4 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
154153raleqdv 3136 . . 3 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (∀𝑥 ∈ ( 𝑅 × 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)))))
155151, 154mpbid 222 . 2 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
156 eqid 2621 . . 3 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
157156is1stc2 21168 . 2 ((𝑅 ×t 𝑆) ∈ 1st𝜔 ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑥 (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)))))
1584, 155, 157sylanbrc 697 1 ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ×t 𝑆) ∈ 1st𝜔)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  {cab 2607  wral 2907  wrex 2908  wss 3559  𝒫 cpw 4135  cop 4159   cuni 4407   class class class wbr 4618   × cxp 5077  dom cdm 5079  ran crn 5080  Oncon0 5687   Fn wfn 5847  wf 5848  ontowfo 5850  (class class class)co 6610  cmpt2 6612  ωcom 7019  cen 7904  cdom 7905  cardccrd 8713  Topctop 20630  1st𝜔c1stc 21163   ×t ctx 21286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-oi 8367  df-card 8717  df-acn 8720  df-topgen 16036  df-top 20631  df-topon 20648  df-bases 20674  df-1stc 21165  df-tx 21288
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator