Step | Hyp | Ref
| Expression |
1 | | pwuni 4878 |
. . . . . . . . . 10
⊢
〈𝑥, 𝑦〉 ⊆ 𝒫 ∪ 〈𝑥, 𝑦〉 |
2 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
3 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
4 | 2, 3 | uniop 5429 |
. . . . . . . . . . 11
⊢ ∪ 〈𝑥, 𝑦〉 = {𝑥, 𝑦} |
5 | 4 | pweqi 4551 |
. . . . . . . . . 10
⊢ 𝒫
∪ 〈𝑥, 𝑦〉 = 𝒫 {𝑥, 𝑦} |
6 | 1, 5 | sseqtri 3957 |
. . . . . . . . 9
⊢
〈𝑥, 𝑦〉 ⊆ 𝒫 {𝑥, 𝑦} |
7 | | pwuni 4878 |
. . . . . . . . . . 11
⊢ {𝑥, 𝑦} ⊆ 𝒫 ∪ {𝑥,
𝑦} |
8 | 2, 3 | unipr 4857 |
. . . . . . . . . . . 12
⊢ ∪ {𝑥,
𝑦} = (𝑥 ∪ 𝑦) |
9 | 8 | pweqi 4551 |
. . . . . . . . . . 11
⊢ 𝒫
∪ {𝑥, 𝑦} = 𝒫 (𝑥 ∪ 𝑦) |
10 | 7, 9 | sseqtri 3957 |
. . . . . . . . . 10
⊢ {𝑥, 𝑦} ⊆ 𝒫 (𝑥 ∪ 𝑦) |
11 | 10 | sspwi 4547 |
. . . . . . . . 9
⊢ 𝒫
{𝑥, 𝑦} ⊆ 𝒫 𝒫 (𝑥 ∪ 𝑦) |
12 | 6, 11 | sstri 3930 |
. . . . . . . 8
⊢
〈𝑥, 𝑦〉 ⊆ 𝒫
𝒫 (𝑥 ∪ 𝑦) |
13 | 2, 3 | unex 7596 |
. . . . . . . . . . 11
⊢ (𝑥 ∪ 𝑦) ∈ V |
14 | 13 | pwex 5303 |
. . . . . . . . . 10
⊢ 𝒫
(𝑥 ∪ 𝑦) ∈ V |
15 | 14 | pwex 5303 |
. . . . . . . . 9
⊢ 𝒫
𝒫 (𝑥 ∪ 𝑦) ∈ V |
16 | 15 | rankss 9607 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ⊆ 𝒫
𝒫 (𝑥 ∪ 𝑦) → (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘𝒫
𝒫 (𝑥 ∪ 𝑦))) |
17 | 12, 16 | ax-mp 5 |
. . . . . . 7
⊢
(rank‘〈𝑥,
𝑦〉) ⊆
(rank‘𝒫 𝒫 (𝑥 ∪ 𝑦)) |
18 | | rankxplim.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
19 | 18 | rankel 9597 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)) |
20 | | rankxplim.2 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
21 | 20 | rankel 9597 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 → (rank‘𝑦) ∈ (rank‘𝐵)) |
22 | 2, 3, 18, 20 | rankelun 9630 |
. . . . . . . . . 10
⊢
(((rank‘𝑥)
∈ (rank‘𝐴) ∧
(rank‘𝑦) ∈
(rank‘𝐵)) →
(rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) |
23 | 19, 21, 22 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) |
24 | 23 | adantl 482 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) |
25 | | ranklim 9602 |
. . . . . . . . . 10
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → ((rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘𝒫 (𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
26 | | ranklim 9602 |
. . . . . . . . . 10
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → ((rank‘𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
27 | 25, 26 | bitrd 278 |
. . . . . . . . 9
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → ((rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
28 | 27 | adantr 481 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((rank‘(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
29 | 24, 28 | mpbid 231 |
. . . . . . 7
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) |
30 | | rankon 9553 |
. . . . . . . 8
⊢
(rank‘〈𝑥,
𝑦〉) ∈
On |
31 | | rankon 9553 |
. . . . . . . 8
⊢
(rank‘(𝐴 ∪
𝐵)) ∈
On |
32 | | ontr2 6313 |
. . . . . . . 8
⊢
(((rank‘〈𝑥, 𝑦〉) ∈ On ∧ (rank‘(𝐴 ∪ 𝐵)) ∈ On) →
(((rank‘〈𝑥,
𝑦〉) ⊆
(rank‘𝒫 𝒫 (𝑥 ∪ 𝑦)) ∧ (rank‘𝒫 𝒫
(𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) → (rank‘〈𝑥, 𝑦〉) ∈ (rank‘(𝐴 ∪ 𝐵)))) |
33 | 30, 31, 32 | mp2an 689 |
. . . . . . 7
⊢
(((rank‘〈𝑥, 𝑦〉) ⊆ (rank‘𝒫
𝒫 (𝑥 ∪ 𝑦)) ∧ (rank‘𝒫
𝒫 (𝑥 ∪ 𝑦)) ∈ (rank‘(𝐴 ∪ 𝐵))) → (rank‘〈𝑥, 𝑦〉) ∈ (rank‘(𝐴 ∪ 𝐵))) |
34 | 17, 29, 33 | sylancr 587 |
. . . . . 6
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (rank‘〈𝑥, 𝑦〉) ∈ (rank‘(𝐴 ∪ 𝐵))) |
35 | 30, 31 | onsucssi 7688 |
. . . . . 6
⊢
((rank‘〈𝑥, 𝑦〉) ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
36 | 34, 35 | sylib 217 |
. . . . 5
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
37 | 36 | ralrimivva 3123 |
. . . 4
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
38 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (rank‘𝑧) = (rank‘〈𝑥, 𝑦〉)) |
39 | | suceq 6331 |
. . . . . . . 8
⊢
((rank‘𝑧) =
(rank‘〈𝑥, 𝑦〉) → suc
(rank‘𝑧) = suc
(rank‘〈𝑥, 𝑦〉)) |
40 | 38, 39 | syl 17 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → suc (rank‘𝑧) = suc (rank‘〈𝑥, 𝑦〉)) |
41 | 40 | sseq1d 3952 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (suc (rank‘𝑧) ⊆ (rank‘(𝐴 ∪ 𝐵)) ↔ suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵)))) |
42 | 41 | ralxp 5750 |
. . . . 5
⊢
(∀𝑧 ∈
(𝐴 × 𝐵)suc (rank‘𝑧) ⊆ (rank‘(𝐴 ∪ 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
43 | 18, 20 | xpex 7603 |
. . . . . 6
⊢ (𝐴 × 𝐵) ∈ V |
44 | 43 | rankbnd 9626 |
. . . . 5
⊢
(∀𝑧 ∈
(𝐴 × 𝐵)suc (rank‘𝑧) ⊆ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘(𝐴 × 𝐵)) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
45 | 42, 44 | bitr3i 276 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 suc (rank‘〈𝑥, 𝑦〉) ⊆ (rank‘(𝐴 ∪ 𝐵)) ↔ (rank‘(𝐴 × 𝐵)) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
46 | 37, 45 | sylib 217 |
. . 3
⊢ (Lim
(rank‘(𝐴 ∪ 𝐵)) → (rank‘(𝐴 × 𝐵)) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
47 | 46 | adantr 481 |
. 2
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
48 | 18, 20 | rankxpl 9633 |
. . 3
⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
49 | 48 | adantl 482 |
. 2
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
50 | 47, 49 | eqssd 3938 |
1
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |