Step | Hyp | Ref
| Expression |
1 | | 1stctop 21056 |
. . 3
⊢ (𝑅 ∈ 1st𝜔
→ 𝑅 ∈
Top) |
2 | | 1stctop 21056 |
. . 3
⊢ (𝑆 ∈ 1st𝜔
→ 𝑆 ∈
Top) |
3 | | txtop 21182 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) |
4 | 1, 2, 3 | syl2an 493 |
. 2
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (𝑅 ×t 𝑆) ∈ Top) |
5 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝑅 =
∪ 𝑅 |
6 | 5 | 1stcclb 21057 |
. . . . . . 7
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑢 ∈ ∪ 𝑅)
→ ∃𝑎 ∈
𝒫 𝑅(𝑎 ≼ ω ∧
∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)))) |
7 | 6 | ad2ant2r 779 |
. . . . . 6
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)))) |
8 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝑆 =
∪ 𝑆 |
9 | 8 | 1stcclb 21057 |
. . . . . . 7
⊢ ((𝑆 ∈ 1st𝜔
∧ 𝑣 ∈ ∪ 𝑆)
→ ∃𝑏 ∈
𝒫 𝑆(𝑏 ≼ ω ∧
∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) |
10 | 9 | ad2ant2l 778 |
. . . . . 6
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) |
11 | | reeanv 3086 |
. . . . . . 7
⊢
(∃𝑎 ∈
𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) |
12 | | an4 861 |
. . . . . . . . 9
⊢ (((𝑎 ≼ ω ∧
∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) |
13 | | txopn 21215 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚 ∈ 𝑅 ∧ 𝑛 ∈ 𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
14 | 13 | ralrimivva 2954 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
15 | 1, 2, 14 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
17 | | elpwi 4117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ 𝒫 𝑅 → 𝑎 ⊆ 𝑅) |
18 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ⊆ 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ 𝒫 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
20 | | elpwi 4117 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ 𝒫 𝑆 → 𝑏 ⊆ 𝑆) |
21 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ⊆ 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
23 | 22 | ralimdv 2946 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
24 | 19, 23 | sylan9 687 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆) → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
25 | 16, 24 | mpan9 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
26 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) |
27 | 26 | fmpt2 7126 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆)) |
28 | 25, 27 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆)) |
29 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) |
31 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ×t 𝑆) ∈ V |
32 | 31 | elpw2 4755 |
. . . . . . . . . . . . 13
⊢ (ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) |
33 | 30, 32 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆)) |
34 | 33 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆)) |
35 | | omelon 8426 |
. . . . . . . . . . . . . . 15
⊢ ω
∈ On |
36 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑏 ∈ V |
37 | 36 | xpdom1 7944 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ≼ ω → (𝑎 × 𝑏) ≼ (ω × 𝑏)) |
38 | | omex 8423 |
. . . . . . . . . . . . . . . . . 18
⊢ ω
∈ V |
39 | 38 | xpdom2 7940 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ≼ ω → (ω
× 𝑏) ≼ (ω
× ω)) |
40 | | domtr 7895 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 × 𝑏) ≼ (ω × 𝑏) ∧ (ω × 𝑏) ≼ (ω × ω)) →
(𝑎 × 𝑏) ≼ (ω ×
ω)) |
41 | 37, 39, 40 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ (ω ×
ω)) |
42 | | xpomen 8721 |
. . . . . . . . . . . . . . . 16
⊢ (ω
× ω) ≈ ω |
43 | | domentr 7901 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 × 𝑏) ≼ (ω × ω) ∧
(ω × ω) ≈ ω) → (𝑎 × 𝑏) ≼ ω) |
44 | 41, 42, 43 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω) |
45 | | ondomen 8743 |
. . . . . . . . . . . . . . 15
⊢ ((ω
∈ On ∧ (𝑎 ×
𝑏) ≼ ω) →
(𝑎 × 𝑏) ∈ dom
card) |
46 | 35, 44, 45 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card) |
47 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑚 ∈ V |
48 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑛 ∈ V |
49 | 47, 48 | xpex 6860 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 × 𝑛) ∈ V |
50 | 26, 49 | fnmpt2i 7128 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) |
51 | | dffn4 6034 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))) |
52 | 50, 51 | mpbi 219 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) |
53 | | fodomnum 8763 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 × 𝑏) ∈ dom card → ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))) |
54 | 46, 52, 53 | mpisyl 21 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)) |
55 | | domtr 7895 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) |
56 | 54, 44, 55 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) |
57 | 56 | ad2antrl 760 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) |
58 | 1, 2 | anim12i 588 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top)) |
59 | 58 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top)) |
60 | | eltx 21181 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
62 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (𝑤 ∈ (𝑟 × 𝑠) ↔ 〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠))) |
63 | 62 | anbi1d 737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
64 | 63 | 2rexbidv 3039 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
65 | 64 | rspccv 3279 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
66 | | r19.27v 3052 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑟 ∈
𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) |
67 | | r19.29 3054 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑟 ∈
𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
68 | | r19.29 3054 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑠 ∈
𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
69 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ↔ (𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠)) |
70 | | pm3.35 609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) |
71 | | pm3.35 609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) |
72 | 70, 71 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
73 | 72 | an4s 865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
74 | 69, 73 | sylanb 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
75 | 74 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
76 | 75 | anasss 677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
77 | 76 | an12s 839 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
78 | 77 | expl 646 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
79 | 78 | reximdv 2999 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
80 | 68, 79 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
81 | 80 | impl 648 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
82 | 81 | reximi 2994 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑟 ∈
𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
83 | 67, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑟 ∈
𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
84 | 66, 83 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢
(((∀𝑟 ∈
𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
85 | | reeanv 3086 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑝 ∈
𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ↔ (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
86 | | simpr1l 1111 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝 ∈ 𝑎) |
87 | | simpr1r 1112 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞 ∈ 𝑏) |
88 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞)) |
89 | | xpeq1 5052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛)) |
90 | 89 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛))) |
91 | | xpeq2 5053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞)) |
92 | 91 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞))) |
93 | 90, 92 | rspc2ev 3295 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) |
94 | 86, 87, 88, 93 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) |
95 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑝 ∈ V |
96 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑞 ∈ V |
97 | 95, 96 | xpex 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 × 𝑞) ∈ V |
98 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛))) |
99 | 98 | 2rexbidv 3039 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (𝑝 × 𝑞) → (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))) |
100 | 97, 99 | elab 3319 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) |
101 | 94, 100 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)}) |
102 | 26 | rnmpt2 6668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} |
103 | 101, 102 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))) |
104 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
105 | | opelxpi 5072 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 ∈ 𝑝 ∧ 𝑣 ∈ 𝑞) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) |
106 | 105 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) |
107 | 104, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) |
108 | | xpss12 5148 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ⊆ 𝑟 ∧ 𝑞 ⊆ 𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) |
109 | 108 | ad2ant2l 778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) |
110 | 104, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) |
111 | | simpr3 1062 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧) |
112 | 110, 111 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧) |
113 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (𝑝 × 𝑞) → (〈𝑢, 𝑣〉 ∈ 𝑤 ↔ 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞))) |
114 | | sseq1 3589 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (𝑝 × 𝑞) → (𝑤 ⊆ 𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧)) |
115 | 113, 114 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = (𝑝 × 𝑞) → ((〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧))) |
116 | 115 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
117 | 103, 107,
112, 116 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
118 | 117 | 3exp2 1277 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) → (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
119 | 118 | rexlimdvv 3019 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
120 | 85, 119 | syl5bir 232 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
121 | 120 | impd 446 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
122 | 121 | rexlimdvva 3020 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
123 | 84, 122 | syl5 33 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
124 | 123 | expd 451 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
125 | 124 | impr 647 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
126 | 65, 125 | syl9r 76 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
127 | 61, 126 | sylbid 229 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
128 | 127 | ralrimiv 2948 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
129 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)) |
130 | | rexeq 3116 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
131 | 130 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
132 | 131 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
133 | 129, 132 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
134 | 133 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
135 | 34, 57, 128, 134 | syl12anc 1316 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
136 | 135 | ex 449 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
137 | 12, 136 | syl5bi 231 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
138 | 137 | rexlimdvva 3020 |
. . . . . . 7
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
139 | 11, 138 | syl5bir 232 |
. . . . . 6
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
140 | 7, 10, 139 | mp2and 711 |
. . . . 5
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
141 | 140 | ralrimivva 2954 |
. . . 4
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
142 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (𝑥 ∈ 𝑧 ↔ 〈𝑢, 𝑣〉 ∈ 𝑧)) |
143 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (𝑥 ∈ 𝑤 ↔ 〈𝑢, 𝑣〉 ∈ 𝑤)) |
144 | 143 | anbi1d 737 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
145 | 144 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
146 | 142, 145 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
147 | 146 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
148 | 147 | anbi2d 736 |
. . . . . 6
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
149 | 148 | rexbidv 3034 |
. . . . 5
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
150 | 149 | ralxp 5185 |
. . . 4
⊢
(∀𝑥 ∈
(∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
151 | 141, 150 | sylibr 223 |
. . 3
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
152 | 5, 8 | txuni 21205 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
153 | 1, 2, 152 | syl2an 493 |
. . . 4
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (∪ 𝑅 × ∪ 𝑆) = ∪
(𝑅 ×t
𝑆)) |
154 | 153 | raleqdv 3121 |
. . 3
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
155 | 151, 154 | mpbid 221 |
. 2
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
156 | | eqid 2610 |
. . 3
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
157 | 156 | is1stc2 21055 |
. 2
⊢ ((𝑅 ×t 𝑆) ∈ 1st𝜔
↔ ((𝑅
×t 𝑆)
∈ Top ∧ ∀𝑥
∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
158 | 4, 155, 157 | sylanbrc 695 |
1
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (𝑅 ×t 𝑆) ∈
1st𝜔) |