| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1stctop 23452 | . . 3
⊢ (𝑅 ∈ 1stω
→ 𝑅 ∈
Top) | 
| 2 |  | 1stctop 23452 | . . 3
⊢ (𝑆 ∈ 1stω
→ 𝑆 ∈
Top) | 
| 3 |  | txtop 23578 | . . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) | 
| 4 | 1, 2, 3 | syl2an 596 | . 2
⊢ ((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) → (𝑅 ×t 𝑆) ∈ Top) | 
| 5 |  | eqid 2736 | . . . . . . . 8
⊢ ∪ 𝑅 =
∪ 𝑅 | 
| 6 | 5 | 1stcclb 23453 | . . . . . . 7
⊢ ((𝑅 ∈ 1stω
∧ 𝑢 ∈ ∪ 𝑅)
→ ∃𝑎 ∈
𝒫 𝑅(𝑎 ≼ ω ∧
∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)))) | 
| 7 | 6 | ad2ant2r 747 | . . . . . 6
⊢ (((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)))) | 
| 8 |  | eqid 2736 | . . . . . . . 8
⊢ ∪ 𝑆 =
∪ 𝑆 | 
| 9 | 8 | 1stcclb 23453 | . . . . . . 7
⊢ ((𝑆 ∈ 1stω
∧ 𝑣 ∈ ∪ 𝑆)
→ ∃𝑏 ∈
𝒫 𝑆(𝑏 ≼ ω ∧
∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) | 
| 10 | 9 | ad2ant2l 746 | . . . . . 6
⊢ (((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) | 
| 11 |  | reeanv 3228 | . . . . . . 7
⊢
(∃𝑎 ∈
𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) | 
| 12 |  | an4 656 | . . . . . . . . 9
⊢ (((𝑎 ≼ ω ∧
∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) | 
| 13 |  | txopn 23611 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚 ∈ 𝑅 ∧ 𝑛 ∈ 𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) | 
| 14 | 13 | ralrimivva 3201 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) | 
| 15 | 1, 2, 14 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) | 
| 16 | 15 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) | 
| 17 |  | elpwi 4606 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ 𝒫 𝑅 → 𝑎 ⊆ 𝑅) | 
| 18 |  | ssralv 4051 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ⊆ 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ 𝒫 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) | 
| 20 |  | elpwi 4606 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ 𝒫 𝑆 → 𝑏 ⊆ 𝑆) | 
| 21 |  | ssralv 4051 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ⊆ 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) | 
| 22 | 20, 21 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) | 
| 23 | 22 | ralimdv 3168 | . . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) | 
| 24 | 19, 23 | sylan9 507 | . . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆) → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) | 
| 25 | 16, 24 | mpan9 506 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) | 
| 26 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) | 
| 27 | 26 | fmpo 8094 | . . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆)) | 
| 28 | 25, 27 | sylib 218 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆)) | 
| 29 | 28 | frnd 6743 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) | 
| 30 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢ (𝑅 ×t 𝑆) ∈ V | 
| 31 | 30 | elpw2 5333 | . . . . . . . . . . . . 13
⊢ (ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) | 
| 32 | 29, 31 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆)) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . 11
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆)) | 
| 34 |  | omelon 9687 | . . . . . . . . . . . . . . 15
⊢ ω
∈ On | 
| 35 |  | xpct 10057 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω) | 
| 36 |  | ondomen 10078 | . . . . . . . . . . . . . . 15
⊢ ((ω
∈ On ∧ (𝑎 ×
𝑏) ≼ ω) →
(𝑎 × 𝑏) ∈ dom
card) | 
| 37 | 34, 35, 36 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card) | 
| 38 |  | vex 3483 | . . . . . . . . . . . . . . . . 17
⊢ 𝑚 ∈ V | 
| 39 |  | vex 3483 | . . . . . . . . . . . . . . . . 17
⊢ 𝑛 ∈ V | 
| 40 | 38, 39 | xpex 7774 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 × 𝑛) ∈ V | 
| 41 | 26, 40 | fnmpoi 8096 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) | 
| 42 |  | dffn4 6825 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))) | 
| 43 | 41, 42 | mpbi 230 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) | 
| 44 |  | fodomnum 10098 | . . . . . . . . . . . . . 14
⊢ ((𝑎 × 𝑏) ∈ dom card → ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))) | 
| 45 | 37, 43, 44 | mpisyl 21 | . . . . . . . . . . . . 13
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)) | 
| 46 |  | domtr 9048 | . . . . . . . . . . . . 13
⊢ ((ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) | 
| 47 | 45, 35, 46 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) | 
| 48 | 47 | ad2antrl 728 | . . . . . . . . . . 11
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) | 
| 49 | 1, 2 | anim12i 613 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top)) | 
| 50 | 49 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top)) | 
| 51 |  | eltx 23577 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 52 | 50, 51 | syl 17 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 53 |  | eleq1 2828 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (𝑤 ∈ (𝑟 × 𝑠) ↔ 〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠))) | 
| 54 | 53 | anbi1d 631 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 55 | 54 | 2rexbidv 3221 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 56 | 55 | rspccv 3618 | . . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 57 |  | r19.27v 3187 | . . . . . . . . . . . . . . . . . 18
⊢
((∀𝑟 ∈
𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) | 
| 58 |  | r19.29 3113 | . . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑟 ∈
𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 59 |  | r19.29 3113 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑠 ∈
𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 60 |  | opelxp 5720 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ↔ (𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠)) | 
| 61 |  | pm3.35 802 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) | 
| 62 |  | pm3.35 802 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) | 
| 63 | 61, 62 | anim12i 613 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) | 
| 64 | 63 | an4s 660 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) | 
| 65 | 60, 64 | sylanb 581 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) | 
| 66 | 65 | anim1i 615 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) | 
| 67 | 66 | anasss 466 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) | 
| 68 | 67 | an12s 649 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) | 
| 69 | 68 | expl 457 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 70 | 69 | reximdv 3169 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 71 | 59, 70 | syl5 34 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) | 
| 72 | 71 | impl 455 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) | 
| 73 | 72 | reximi 3083 | . . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑟 ∈
𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) | 
| 74 | 58, 73 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
((∀𝑟 ∈
𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) | 
| 75 | 57, 74 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢
(((∀𝑟 ∈
𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) | 
| 76 |  | reeanv 3228 | . . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑝 ∈
𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ↔ (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) | 
| 77 |  | simpr1l 1230 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝 ∈ 𝑎) | 
| 78 |  | simpr1r 1231 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞 ∈ 𝑏) | 
| 79 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞)) | 
| 80 |  | xpeq1 5698 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛)) | 
| 81 | 80 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛))) | 
| 82 |  | xpeq2 5705 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞)) | 
| 83 | 82 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞))) | 
| 84 | 81, 83 | rspc2ev 3634 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) | 
| 85 | 77, 78, 79, 84 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) | 
| 86 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑝 ∈ V | 
| 87 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑞 ∈ V | 
| 88 | 86, 87 | xpex 7774 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 × 𝑞) ∈ V | 
| 89 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛))) | 
| 90 | 89 | 2rexbidv 3221 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (𝑝 × 𝑞) → (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))) | 
| 91 | 88, 90 | elab 3678 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) | 
| 92 | 85, 91 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)}) | 
| 93 | 26 | rnmpo 7567 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} | 
| 94 | 92, 93 | eleqtrrdi 2851 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))) | 
| 95 |  | simpr2 1195 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) | 
| 96 |  | opelxpi 5721 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 ∈ 𝑝 ∧ 𝑣 ∈ 𝑞) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) | 
| 97 | 96 | ad2ant2r 747 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) | 
| 98 | 95, 97 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) | 
| 99 |  | xpss12 5699 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ⊆ 𝑟 ∧ 𝑞 ⊆ 𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) | 
| 100 | 99 | ad2ant2l 746 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) | 
| 101 | 95, 100 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) | 
| 102 |  | simpr3 1196 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧) | 
| 103 | 101, 102 | sstrd 3993 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧) | 
| 104 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (𝑝 × 𝑞) → (〈𝑢, 𝑣〉 ∈ 𝑤 ↔ 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞))) | 
| 105 |  | sseq1 4008 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (𝑝 × 𝑞) → (𝑤 ⊆ 𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧)) | 
| 106 | 104, 105 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = (𝑝 × 𝑞) → ((〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧))) | 
| 107 | 106 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) | 
| 108 | 94, 98, 103, 107 | syl12anc 836 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) | 
| 109 | 108 | 3exp2 1354 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) → (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | 
| 110 | 109 | rexlimdvv 3211 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 111 | 76, 110 | biimtrrid 243 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 112 | 111 | impd 410 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) | 
| 113 | 112 | rexlimdvva 3212 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) | 
| 114 | 75, 113 | syl5 34 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) | 
| 115 | 114 | expd 415 | . . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 116 | 115 | impr 454 | . . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) | 
| 117 | 56, 116 | syl9r 78 | . . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 118 | 52, 117 | sylbid 240 | . . . . . . . . . . . 12
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 119 | 118 | ralrimiv 3144 | . . . . . . . . . . 11
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) | 
| 120 |  | breq1 5145 | . . . . . . . . . . . . 13
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)) | 
| 121 |  | rexeq 3321 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) | 
| 122 | 121 | imbi2d 340 | . . . . . . . . . . . . . 14
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 123 | 122 | ralbidv 3177 | . . . . . . . . . . . . 13
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 124 | 120, 123 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | 
| 125 | 124 | rspcev 3621 | . . . . . . . . . . 11
⊢ ((ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 126 | 33, 48, 119, 125 | syl12anc 836 | . . . . . . . . . 10
⊢
(((((𝑅 ∈
1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 127 | 126 | ex 412 | . . . . . . . . 9
⊢ ((((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | 
| 128 | 12, 127 | biimtrid 242 | . . . . . . . 8
⊢ ((((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | 
| 129 | 128 | rexlimdvva 3212 | . . . . . . 7
⊢ (((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | 
| 130 | 11, 129 | biimtrrid 243 | . . . . . 6
⊢ (((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | 
| 131 | 7, 10, 130 | mp2and 699 | . . . . 5
⊢ (((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 132 | 131 | ralrimivva 3201 | . . . 4
⊢ ((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) → ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 133 |  | eleq1 2828 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (𝑥 ∈ 𝑧 ↔ 〈𝑢, 𝑣〉 ∈ 𝑧)) | 
| 134 |  | eleq1 2828 | . . . . . . . . . . 11
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (𝑥 ∈ 𝑤 ↔ 〈𝑢, 𝑣〉 ∈ 𝑤)) | 
| 135 | 134 | anbi1d 631 | . . . . . . . . . 10
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) | 
| 136 | 135 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) | 
| 137 | 133, 136 | imbi12d 344 | . . . . . . . 8
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 138 | 137 | ralbidv 3177 | . . . . . . 7
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 139 | 138 | anbi2d 630 | . . . . . 6
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | 
| 140 | 139 | rexbidv 3178 | . . . . 5
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | 
| 141 | 140 | ralxp 5851 | . . . 4
⊢
(∀𝑥 ∈
(∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 142 | 132, 141 | sylibr 234 | . . 3
⊢ ((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) → ∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 143 | 5, 8 | txuni 23601 | . . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) | 
| 144 | 1, 2, 143 | syl2an 596 | . . 3
⊢ ((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) → (∪ 𝑅 × ∪ 𝑆) = ∪
(𝑅 ×t
𝑆)) | 
| 145 | 142, 144 | raleqtrdv 3327 | . 2
⊢ ((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) → ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) | 
| 146 |  | eqid 2736 | . . 3
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) | 
| 147 | 146 | is1stc2 23451 | . 2
⊢ ((𝑅 ×t 𝑆) ∈ 1stω
↔ ((𝑅
×t 𝑆)
∈ Top ∧ ∀𝑥
∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | 
| 148 | 4, 145, 147 | sylanbrc 583 | 1
⊢ ((𝑅 ∈ 1stω
∧ 𝑆 ∈
1stω) → (𝑅 ×t 𝑆) ∈
1stω) |