Step | Hyp | Ref
| Expression |
1 | | pwuni 4711 |
. . . . . . . . . 10
⊢
〈𝑥, 𝑦〉 ⊆ 𝒫 ∪ 〈𝑥, 𝑦〉 |
2 | | vex 3401 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
3 | | vex 3401 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
4 | 2, 3 | uniop 5214 |
. . . . . . . . . . 11
⊢ ∪ 〈𝑥, 𝑦〉 = {𝑥, 𝑦} |
5 | 4 | pweqi 4383 |
. . . . . . . . . 10
⊢ 𝒫
∪ 〈𝑥, 𝑦〉 = 𝒫 {𝑥, 𝑦} |
6 | 1, 5 | sseqtri 3856 |
. . . . . . . . 9
⊢
〈𝑥, 𝑦〉 ⊆ 𝒫 {𝑥, 𝑦} |
7 | | pwuni 4711 |
. . . . . . . . . . 11
⊢ {𝑥, 𝑦} ⊆ 𝒫 ∪ {𝑥,
𝑦} |
8 | 2, 3 | unipr 4686 |
. . . . . . . . . . . 12
⊢ ∪ {𝑥,
𝑦} = (𝑥 ∪ 𝑦) |
9 | 8 | pweqi 4383 |
. . . . . . . . . . 11
⊢ 𝒫
∪ {𝑥, 𝑦} = 𝒫 (𝑥 ∪ 𝑦) |
10 | 7, 9 | sseqtri 3856 |
. . . . . . . . . 10
⊢ {𝑥, 𝑦} ⊆ 𝒫 (𝑥 ∪ 𝑦) |
11 | | sspwb 5151 |
. . . . . . . . . 10
⊢ ({𝑥, 𝑦} ⊆ 𝒫 (𝑥 ∪ 𝑦) ↔ 𝒫 {𝑥, 𝑦} ⊆ 𝒫 𝒫 (𝑥 ∪ 𝑦)) |
12 | 10, 11 | mpbi 222 |
. . . . . . . . 9
⊢ 𝒫
{𝑥, 𝑦} ⊆ 𝒫 𝒫 (𝑥 ∪ 𝑦) |
13 | 6, 12 | sstri 3830 |
. . . . . . . 8
⊢
〈𝑥, 𝑦〉 ⊆ 𝒫
𝒫 (𝑥 ∪ 𝑦) |
14 | 2, 3 | unex 7235 |
. . . . . . . . . . 11
⊢ (𝑥 ∪ 𝑦) ∈ V |
15 | 14 | pwex 5094 |
. . . . . . . . . 10
⊢ 𝒫
(𝑥 ∪ 𝑦) ∈ V |
16 | 15 | pwex 5094 |
. . . . . . . . 9
⊢ 𝒫
𝒫 (𝑥 ∪ 𝑦) ∈ V |
17 | 16 | rankss 9011 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ⊆ 𝒫
𝒫 (𝑥 ∪ 𝑦) → (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘𝒫
𝒫 (𝑥 ∪ 𝑦))) |
18 | 13, 17 | ax-mp 5 |
. . . . . . 7
⊢
(rank‘〈𝑥,
𝑦〉) ⊆
(rank‘𝒫 𝒫 (𝑥 ∪ 𝑦)) |
19 | | rankxplim.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
20 | 19 | rankel 9001 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)) |
21 | | rankxplim.2 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
22 | 21 | rankel 9001 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 → (rank‘𝑦) ∈ (rank‘𝐵)) |
23 | 2, 3, 19, 21 | rankelun 9034 |
. . . . . . . . . 10
⊢
(((rank‘𝑥)
∈ (rank‘𝐴) ∧
(rank‘𝑦) ∈
(rank‘𝐵)) →
(rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) |
24 | 20, 22, 23 | syl2an 589 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) |
25 | 24 | adantl 475 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) |
26 | | ranklim 9006 |
. . . . . . . . . 10
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → ((rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘𝒫 (𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
27 | | ranklim 9006 |
. . . . . . . . . 10
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → ((rank‘𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
28 | 26, 27 | bitrd 271 |
. . . . . . . . 9
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → ((rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
29 | 28 | adantr 474 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
30 | 25, 29 | mpbid 224 |
. . . . . . 7
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) |
31 | | rankon 8957 |
. . . . . . . 8
⊢
(rank‘〈𝑥,
𝑦〉) ∈
On |
32 | | rankon 8957 |
. . . . . . . 8
⊢
(rank‘(𝐴 ∪
𝐵)) ∈
On |
33 | | ontr2 6025 |
. . . . . . . 8
⊢
(((rank‘〈𝑥, 𝑦〉) ∈ On ∧ (rank‘(𝐴 ∪ 𝐵)) ∈ On) →
(((rank‘〈𝑥,
𝑦〉) ⊆
(rank‘𝒫 𝒫 (𝑥 ∪ 𝑦)) ∧ (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) → (rank‘〈𝑥, 𝑦〉) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
34 | 31, 32, 33 | mp2an 682 |
. . . . . . 7
⊢
(((rank‘〈𝑥, 𝑦〉) ⊆ (rank‘𝒫
𝒫 (𝑥 ∪ 𝑦)) ∧ (rank‘𝒫
𝒫 (𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) → (rank‘〈𝑥, 𝑦〉) ∈ (rank‘(𝐴 ∪ 𝐵))) |
35 | 18, 30, 34 | sylancr 581 |
. . . . . 6
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (rank‘〈𝑥, 𝑦〉) ∈ (rank‘(𝐴 ∪ 𝐵))) |
36 | 31, 32 | onsucssi 7321 |
. . . . . 6
⊢
((rank‘〈𝑥, 𝑦〉) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
37 | 35, 36 | sylib 210 |
. . . . 5
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
38 | 37 | ralrimivva 3153 |
. . . 4
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
39 | | fveq2 6448 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (rank‘𝑧) = (rank‘〈𝑥, 𝑦〉)) |
40 | | suceq 6043 |
. . . . . . . 8
⊢
((rank‘𝑧) =
(rank‘〈𝑥, 𝑦〉) → suc
(rank‘𝑧) = suc
(rank‘〈𝑥, 𝑦〉)) |
41 | 39, 40 | syl 17 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → suc (rank‘𝑧) = suc (rank‘〈𝑥, 𝑦〉)) |
42 | 41 | sseq1d 3851 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (suc (rank‘𝑧) ⊆ (rank‘(𝐴 ∪ 𝐵)) ↔ suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵)))) |
43 | 42 | ralxp 5511 |
. . . . 5
⊢
(∀𝑧 ∈
(𝐴 × 𝐵)suc (rank‘𝑧) ⊆ (rank‘(𝐴 ∪ 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
44 | 19, 21 | xpex 7242 |
. . . . . 6
⊢ (𝐴 × 𝐵) ∈ V |
45 | 44 | rankbnd 9030 |
. . . . 5
⊢
(∀𝑧 ∈
(𝐴 × 𝐵)suc (rank‘𝑧) ⊆ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘(𝐴 × 𝐵)) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
46 | 43, 45 | bitr3i 269 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘(𝐴 × 𝐵)) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
47 | 38, 46 | sylib 210 |
. . 3
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → (rank‘(𝐴 × 𝐵)) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
48 | 47 | adantr 474 |
. 2
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
49 | 19, 21 | rankxpl 9037 |
. . 3
⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
50 | 49 | adantl 475 |
. 2
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
51 | 48, 50 | eqssd 3838 |
1
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |