Step | Hyp | Ref
| Expression |
1 | | 1stctop 21655 |
. . 3
⊢ (𝑅 ∈ 1st𝜔
→ 𝑅 ∈
Top) |
2 | | 1stctop 21655 |
. . 3
⊢ (𝑆 ∈ 1st𝜔
→ 𝑆 ∈
Top) |
3 | | txtop 21781 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) |
4 | 1, 2, 3 | syl2an 589 |
. 2
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (𝑅 ×t 𝑆) ∈ Top) |
5 | | eqid 2778 |
. . . . . . . 8
⊢ ∪ 𝑅 =
∪ 𝑅 |
6 | 5 | 1stcclb 21656 |
. . . . . . 7
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑢 ∈ ∪ 𝑅)
→ ∃𝑎 ∈
𝒫 𝑅(𝑎 ≼ ω ∧
∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)))) |
7 | 6 | ad2ant2r 737 |
. . . . . 6
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)))) |
8 | | eqid 2778 |
. . . . . . . 8
⊢ ∪ 𝑆 =
∪ 𝑆 |
9 | 8 | 1stcclb 21656 |
. . . . . . 7
⊢ ((𝑆 ∈ 1st𝜔
∧ 𝑣 ∈ ∪ 𝑆)
→ ∃𝑏 ∈
𝒫 𝑆(𝑏 ≼ ω ∧
∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) |
10 | 9 | ad2ant2l 736 |
. . . . . 6
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) |
11 | | reeanv 3293 |
. . . . . . 7
⊢
(∃𝑎 ∈
𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) |
12 | | an4 646 |
. . . . . . . . 9
⊢ (((𝑎 ≼ ω ∧
∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) |
13 | | txopn 21814 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚 ∈ 𝑅 ∧ 𝑛 ∈ 𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
14 | 13 | ralrimivva 3153 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
15 | 1, 2, 14 | syl2an 589 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
16 | 15 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
17 | | elpwi 4389 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ 𝒫 𝑅 → 𝑎 ⊆ 𝑅) |
18 | | ssralv 3885 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ⊆ 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ 𝒫 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
20 | | elpwi 4389 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ 𝒫 𝑆 → 𝑏 ⊆ 𝑆) |
21 | | ssralv 3885 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ⊆ 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
23 | 22 | ralimdv 3145 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
24 | 19, 23 | sylan9 503 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆) → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
25 | 16, 24 | mpan9 502 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
26 | | eqid 2778 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) |
27 | 26 | fmpt2 7517 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆)) |
28 | 25, 27 | sylib 210 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆)) |
29 | 28 | frnd 6298 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) |
30 | | ovex 6954 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ×t 𝑆) ∈ V |
31 | 30 | elpw2 5062 |
. . . . . . . . . . . . 13
⊢ (ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) |
32 | 29, 31 | sylibr 226 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆)) |
33 | 32 | adantr 474 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆)) |
34 | | omelon 8840 |
. . . . . . . . . . . . . . 15
⊢ ω
∈ On |
35 | | vex 3401 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑏 ∈ V |
36 | 35 | xpdom1 8347 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ≼ ω → (𝑎 × 𝑏) ≼ (ω × 𝑏)) |
37 | | omex 8837 |
. . . . . . . . . . . . . . . . . 18
⊢ ω
∈ V |
38 | 37 | xpdom2 8343 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ≼ ω → (ω
× 𝑏) ≼ (ω
× ω)) |
39 | | domtr 8294 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 × 𝑏) ≼ (ω × 𝑏) ∧ (ω × 𝑏) ≼ (ω × ω)) →
(𝑎 × 𝑏) ≼ (ω ×
ω)) |
40 | 36, 38, 39 | syl2an 589 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ (ω ×
ω)) |
41 | | xpomen 9171 |
. . . . . . . . . . . . . . . 16
⊢ (ω
× ω) ≈ ω |
42 | | domentr 8300 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 × 𝑏) ≼ (ω × ω) ∧
(ω × ω) ≈ ω) → (𝑎 × 𝑏) ≼ ω) |
43 | 40, 41, 42 | sylancl 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω) |
44 | | ondomen 9193 |
. . . . . . . . . . . . . . 15
⊢ ((ω
∈ On ∧ (𝑎 ×
𝑏) ≼ ω) →
(𝑎 × 𝑏) ∈ dom
card) |
45 | 34, 43, 44 | sylancr 581 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card) |
46 | | vex 3401 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑚 ∈ V |
47 | | vex 3401 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑛 ∈ V |
48 | 46, 47 | xpex 7240 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 × 𝑛) ∈ V |
49 | 26, 48 | fnmpt2i 7519 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) |
50 | | dffn4 6372 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))) |
51 | 49, 50 | mpbi 222 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) |
52 | | fodomnum 9213 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 × 𝑏) ∈ dom card → ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))) |
53 | 45, 51, 52 | mpisyl 21 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)) |
54 | | domtr 8294 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) |
55 | 53, 43, 54 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) |
56 | 55 | ad2antrl 718 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) |
57 | 1, 2 | anim12i 606 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top)) |
58 | 57 | ad3antrrr 720 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top)) |
59 | | eltx 21780 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
61 | | eleq1 2847 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (𝑤 ∈ (𝑟 × 𝑠) ↔ 〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠))) |
62 | 61 | anbi1d 623 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
63 | 62 | 2rexbidv 3242 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
64 | 63 | rspccv 3508 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
65 | | r19.27v 3256 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑟 ∈
𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) |
66 | | r19.29 3258 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑟 ∈
𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
67 | | r19.29 3258 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑠 ∈
𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
68 | | opelxp 5391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ↔ (𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠)) |
69 | | pm3.35 793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) |
70 | | pm3.35 793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) |
71 | 69, 70 | anim12i 606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
72 | 71 | an4s 650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
73 | 68, 72 | sylanb 576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
74 | 73 | anim1i 608 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
75 | 74 | anasss 460 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
76 | 75 | an12s 639 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
77 | 76 | expl 451 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
78 | 77 | reximdv 3197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
79 | 67, 78 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
80 | 79 | impl 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
81 | 80 | reximi 3192 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑟 ∈
𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
82 | 66, 81 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑟 ∈
𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
83 | 65, 82 | sylan 575 |
. . . . . . . . . . . . . . . . 17
⊢
(((∀𝑟 ∈
𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
84 | | reeanv 3293 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑝 ∈
𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ↔ (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
85 | | simpr1l 1262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝 ∈ 𝑎) |
86 | | simpr1r 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞 ∈ 𝑏) |
87 | | eqidd 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞)) |
88 | | xpeq1 5369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛)) |
89 | 88 | eqeq2d 2788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛))) |
90 | | xpeq2 5376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞)) |
91 | 90 | eqeq2d 2788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞))) |
92 | 89, 91 | rspc2ev 3526 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) |
93 | 85, 86, 87, 92 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) |
94 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑝 ∈ V |
95 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑞 ∈ V |
96 | 94, 95 | xpex 7240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 × 𝑞) ∈ V |
97 | | eqeq1 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛))) |
98 | 97 | 2rexbidv 3242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (𝑝 × 𝑞) → (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))) |
99 | 96, 98 | elab 3558 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) |
100 | 93, 99 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)}) |
101 | 26 | rnmpt2 7047 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} |
102 | 100, 101 | syl6eleqr 2870 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))) |
103 | | simpr2 1207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
104 | | opelxpi 5392 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 ∈ 𝑝 ∧ 𝑣 ∈ 𝑞) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) |
105 | 104 | ad2ant2r 737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) |
106 | 103, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) |
107 | | xpss12 5370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ⊆ 𝑟 ∧ 𝑞 ⊆ 𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) |
108 | 107 | ad2ant2l 736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) |
109 | 103, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) |
110 | | simpr3 1209 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧) |
111 | 109, 110 | sstrd 3831 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧) |
112 | | eleq2 2848 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (𝑝 × 𝑞) → (〈𝑢, 𝑣〉 ∈ 𝑤 ↔ 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞))) |
113 | | sseq1 3845 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (𝑝 × 𝑞) → (𝑤 ⊆ 𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧)) |
114 | 112, 113 | anbi12d 624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = (𝑝 × 𝑞) → ((〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧))) |
115 | 114 | rspcev 3511 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
116 | 102, 106,
111, 115 | syl12anc 827 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
117 | 116 | 3exp2 1416 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) → (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
118 | 117 | rexlimdvv 3220 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
119 | 84, 118 | syl5bir 235 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
120 | 119 | impd 400 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
121 | 120 | rexlimdvva 3221 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
122 | 83, 121 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
123 | 122 | expd 406 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
124 | 123 | impr 448 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
125 | 64, 124 | syl9r 78 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
126 | 60, 125 | sylbid 232 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
127 | 126 | ralrimiv 3147 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
128 | | breq1 4889 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)) |
129 | | rexeq 3331 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
130 | 129 | imbi2d 332 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
131 | 130 | ralbidv 3168 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
132 | 128, 131 | anbi12d 624 |
. . . . . . . . . . . 12
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
133 | 132 | rspcev 3511 |
. . . . . . . . . . 11
⊢ ((ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
134 | 33, 56, 127, 133 | syl12anc 827 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
135 | 134 | ex 403 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
136 | 12, 135 | syl5bi 234 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
137 | 136 | rexlimdvva 3221 |
. . . . . . 7
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
138 | 11, 137 | syl5bir 235 |
. . . . . 6
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
139 | 7, 10, 138 | mp2and 689 |
. . . . 5
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
140 | 139 | ralrimivva 3153 |
. . . 4
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
141 | | eleq1 2847 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (𝑥 ∈ 𝑧 ↔ 〈𝑢, 𝑣〉 ∈ 𝑧)) |
142 | | eleq1 2847 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (𝑥 ∈ 𝑤 ↔ 〈𝑢, 𝑣〉 ∈ 𝑤)) |
143 | 142 | anbi1d 623 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
144 | 143 | rexbidv 3237 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
145 | 141, 144 | imbi12d 336 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
146 | 145 | ralbidv 3168 |
. . . . . . 7
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
147 | 146 | anbi2d 622 |
. . . . . 6
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
148 | 147 | rexbidv 3237 |
. . . . 5
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
149 | 148 | ralxp 5509 |
. . . 4
⊢
(∀𝑥 ∈
(∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
150 | 140, 149 | sylibr 226 |
. . 3
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
151 | 5, 8 | txuni 21804 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
152 | 1, 2, 151 | syl2an 589 |
. . . 4
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (∪ 𝑅 × ∪ 𝑆) = ∪
(𝑅 ×t
𝑆)) |
153 | 152 | raleqdv 3340 |
. . 3
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
154 | 150, 153 | mpbid 224 |
. 2
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
155 | | eqid 2778 |
. . 3
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
156 | 155 | is1stc2 21654 |
. 2
⊢ ((𝑅 ×t 𝑆) ∈ 1st𝜔
↔ ((𝑅
×t 𝑆)
∈ Top ∧ ∀𝑥
∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
157 | 4, 154, 156 | sylanbrc 578 |
1
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (𝑅 ×t 𝑆) ∈
1st𝜔) |