Step | Hyp | Ref
| Expression |
1 | | 1stctop 21294 |
. . 3
⊢ (𝑅 ∈ 1st𝜔
→ 𝑅 ∈
Top) |
2 | | 1stctop 21294 |
. . 3
⊢ (𝑆 ∈ 1st𝜔
→ 𝑆 ∈
Top) |
3 | | txtop 21420 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) |
4 | 1, 2, 3 | syl2an 493 |
. 2
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (𝑅 ×t 𝑆) ∈ Top) |
5 | | eqid 2651 |
. . . . . . . 8
⊢ ∪ 𝑅 =
∪ 𝑅 |
6 | 5 | 1stcclb 21295 |
. . . . . . 7
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑢 ∈ ∪ 𝑅)
→ ∃𝑎 ∈
𝒫 𝑅(𝑎 ≼ ω ∧
∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)))) |
7 | 6 | ad2ant2r 798 |
. . . . . 6
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)))) |
8 | | eqid 2651 |
. . . . . . . 8
⊢ ∪ 𝑆 =
∪ 𝑆 |
9 | 8 | 1stcclb 21295 |
. . . . . . 7
⊢ ((𝑆 ∈ 1st𝜔
∧ 𝑣 ∈ ∪ 𝑆)
→ ∃𝑏 ∈
𝒫 𝑆(𝑏 ≼ ω ∧
∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) |
10 | 9 | ad2ant2l 797 |
. . . . . 6
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) |
11 | | reeanv 3136 |
. . . . . . 7
⊢
(∃𝑎 ∈
𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) |
12 | | an4 882 |
. . . . . . . . 9
⊢ (((𝑎 ≼ ω ∧
∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) |
13 | | txopn 21453 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚 ∈ 𝑅 ∧ 𝑛 ∈ 𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
14 | 13 | ralrimivva 3000 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
15 | 1, 2, 14 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
17 | | elpwi 4201 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ 𝒫 𝑅 → 𝑎 ⊆ 𝑅) |
18 | | ssralv 3699 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ⊆ 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ 𝒫 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
20 | | elpwi 4201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ 𝒫 𝑆 → 𝑏 ⊆ 𝑆) |
21 | | ssralv 3699 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ⊆ 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
23 | 22 | ralimdv 2992 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
24 | 19, 23 | sylan9 690 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆) → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))) |
25 | 16, 24 | mpan9 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)) |
26 | | eqid 2651 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) |
27 | 26 | fmpt2 7282 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆)) |
28 | 25, 27 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆)) |
29 | | frn 6091 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) |
31 | | ovex 6718 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ×t 𝑆) ∈ V |
32 | 31 | elpw2 4858 |
. . . . . . . . . . . . 13
⊢ (ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆)) |
33 | 30, 32 | sylibr 224 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆)) |
34 | 33 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆)) |
35 | | omelon 8581 |
. . . . . . . . . . . . . . 15
⊢ ω
∈ On |
36 | | vex 3234 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑏 ∈ V |
37 | 36 | xpdom1 8100 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ≼ ω → (𝑎 × 𝑏) ≼ (ω × 𝑏)) |
38 | | omex 8578 |
. . . . . . . . . . . . . . . . . 18
⊢ ω
∈ V |
39 | 38 | xpdom2 8096 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ≼ ω → (ω
× 𝑏) ≼ (ω
× ω)) |
40 | | domtr 8050 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 × 𝑏) ≼ (ω × 𝑏) ∧ (ω × 𝑏) ≼ (ω × ω)) →
(𝑎 × 𝑏) ≼ (ω ×
ω)) |
41 | 37, 39, 40 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ (ω ×
ω)) |
42 | | xpomen 8876 |
. . . . . . . . . . . . . . . 16
⊢ (ω
× ω) ≈ ω |
43 | | domentr 8056 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 × 𝑏) ≼ (ω × ω) ∧
(ω × ω) ≈ ω) → (𝑎 × 𝑏) ≼ ω) |
44 | 41, 42, 43 | sylancl 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω) |
45 | | ondomen 8898 |
. . . . . . . . . . . . . . 15
⊢ ((ω
∈ On ∧ (𝑎 ×
𝑏) ≼ ω) →
(𝑎 × 𝑏) ∈ dom
card) |
46 | 35, 44, 45 | sylancr 696 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card) |
47 | | vex 3234 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑚 ∈ V |
48 | | vex 3234 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑛 ∈ V |
49 | 47, 48 | xpex 7004 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 × 𝑛) ∈ V |
50 | 26, 49 | fnmpt2i 7284 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) |
51 | | dffn4 6159 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))) |
52 | 50, 51 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) |
53 | | fodomnum 8918 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 × 𝑏) ∈ dom card → ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))) |
54 | 46, 52, 53 | mpisyl 21 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)) |
55 | | domtr 8050 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) |
56 | 54, 44, 55 | syl2anc 694 |
. . . . . . . . . . . 12
⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) |
57 | 56 | ad2antrl 764 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω) |
58 | 1, 2 | anim12i 589 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top)) |
59 | 58 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top)) |
60 | | eltx 21419 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
62 | | eleq1 2718 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (𝑤 ∈ (𝑟 × 𝑠) ↔ 〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠))) |
63 | 62 | anbi1d 741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
64 | 63 | 2rexbidv 3086 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
65 | 64 | rspccv 3337 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
66 | | r19.27v 3099 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑟 ∈
𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) |
67 | | r19.29 3101 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑟 ∈
𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
68 | | r19.29 3101 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑠 ∈
𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
69 | | opelxp 5180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ↔ (𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠)) |
70 | | pm3.35 610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) |
71 | | pm3.35 610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) |
72 | 70, 71 | anim12i 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
73 | 72 | an4s 886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
74 | 69, 73 | sylanb 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
75 | 74 | anim1i 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
76 | 75 | anasss 680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
77 | 76 | an12s 860 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
78 | 77 | expl 647 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
79 | 78 | reximdv 3045 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
80 | 68, 79 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))) |
81 | 80 | impl 649 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
82 | 81 | reximi 3040 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑟 ∈
𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
83 | 67, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑟 ∈
𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
84 | 66, 83 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢
(((∀𝑟 ∈
𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) |
85 | | reeanv 3136 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑝 ∈
𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ↔ (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
86 | | simpr1l 1138 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝 ∈ 𝑎) |
87 | | simpr1r 1139 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞 ∈ 𝑏) |
88 | | eqidd 2652 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞)) |
89 | | xpeq1 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛)) |
90 | 89 | eqeq2d 2661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛))) |
91 | | xpeq2 5163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞)) |
92 | 91 | eqeq2d 2661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞))) |
93 | 90, 92 | rspc2ev 3355 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) |
94 | 86, 87, 88, 93 | syl3anc 1366 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) |
95 | | vex 3234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑝 ∈ V |
96 | | vex 3234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑞 ∈ V |
97 | 95, 96 | xpex 7004 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 × 𝑞) ∈ V |
98 | | eqeq1 2655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛))) |
99 | 98 | 2rexbidv 3086 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (𝑝 × 𝑞) → (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))) |
100 | 97, 99 | elab 3382 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)) |
101 | 94, 100 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)}) |
102 | 26 | rnmpt2 6812 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} |
103 | 101, 102 | syl6eleqr 2741 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))) |
104 | | simpr2 1088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) |
105 | | opelxpi 5182 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 ∈ 𝑝 ∧ 𝑣 ∈ 𝑞) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) |
106 | 105 | ad2ant2r 798 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) |
107 | 104, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞)) |
108 | | xpss12 5158 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ⊆ 𝑟 ∧ 𝑞 ⊆ 𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) |
109 | 108 | ad2ant2l 797 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) |
110 | 104, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠)) |
111 | | simpr3 1089 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧) |
112 | 110, 111 | sstrd 3646 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧) |
113 | | eleq2 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (𝑝 × 𝑞) → (〈𝑢, 𝑣〉 ∈ 𝑤 ↔ 〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞))) |
114 | | sseq1 3659 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (𝑝 × 𝑞) → (𝑤 ⊆ 𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧)) |
115 | 113, 114 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = (𝑝 × 𝑞) → ((〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧))) |
116 | 115 | rspcev 3340 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∧ (〈𝑢, 𝑣〉 ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
117 | 103, 107,
112, 116 | syl12anc 1364 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
118 | 117 | 3exp2 1307 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) → (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
119 | 118 | rexlimdvv 3066 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
120 | 85, 119 | syl5bir 233 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
121 | 120 | impd 446 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
122 | 121 | rexlimdvva 3067 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
123 | 84, 122 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
124 | 123 | expd 451 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
125 | 124 | impr 648 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
126 | 65, 125 | syl9r 78 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
127 | 61, 126 | sylbid 230 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
128 | 127 | ralrimiv 2994 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
129 | | breq1 4688 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)) |
130 | | rexeq 3169 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
131 | 130 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
132 | 131 | ralbidv 3015 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
133 | 129, 132 | anbi12d 747 |
. . . . . . . . . . . 12
⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
134 | 133 | rspcev 3340 |
. . . . . . . . . . 11
⊢ ((ran
(𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
135 | 34, 57, 128, 134 | syl12anc 1364 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈
1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧
(𝑢 ∈ ∪ 𝑅
∧ 𝑣 ∈ ∪ 𝑆))
∧ (𝑎 ∈ 𝒫
𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
136 | 135 | ex 449 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
137 | 12, 136 | syl5bi 232 |
. . . . . . . 8
⊢ ((((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
138 | 137 | rexlimdvva 3067 |
. . . . . . 7
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
139 | 11, 138 | syl5bir 233 |
. . . . . 6
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
140 | 7, 10, 139 | mp2and 715 |
. . . . 5
⊢ (((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
141 | 140 | ralrimivva 3000 |
. . . 4
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
142 | | eleq1 2718 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (𝑥 ∈ 𝑧 ↔ 〈𝑢, 𝑣〉 ∈ 𝑧)) |
143 | | eleq1 2718 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (𝑥 ∈ 𝑤 ↔ 〈𝑢, 𝑣〉 ∈ 𝑤)) |
144 | 143 | anbi1d 741 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
145 | 144 | rexbidv 3081 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
146 | 142, 145 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
147 | 146 | ralbidv 3015 |
. . . . . . 7
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
148 | 147 | anbi2d 740 |
. . . . . 6
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
149 | 148 | rexbidv 3081 |
. . . . 5
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
150 | 149 | ralxp 5296 |
. . . 4
⊢
(∀𝑥 ∈
(∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(〈𝑢, 𝑣〉 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (〈𝑢, 𝑣〉 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
151 | 141, 150 | sylibr 224 |
. . 3
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
152 | 5, 8 | txuni 21443 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
153 | 1, 2, 152 | syl2an 493 |
. . . 4
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (∪ 𝑅 × ∪ 𝑆) = ∪
(𝑅 ×t
𝑆)) |
154 | 153 | raleqdv 3174 |
. . 3
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
155 | 151, 154 | mpbid 222 |
. 2
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
156 | | eqid 2651 |
. . 3
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
157 | 156 | is1stc2 21293 |
. 2
⊢ ((𝑅 ×t 𝑆) ∈ 1st𝜔
↔ ((𝑅
×t 𝑆)
∈ Top ∧ ∀𝑥
∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
158 | 4, 155, 157 | sylanbrc 699 |
1
⊢ ((𝑅 ∈ 1st𝜔
∧ 𝑆 ∈
1st𝜔) → (𝑅 ×t 𝑆) ∈
1st𝜔) |