Metamath Proof Explorer

Theorem rankxplim

Description: The rank of a Cartesian product when the rank of the union of its arguments is a limit ordinal. Part of Exercise 4 of Kunen p. 107. See rankxpsuc for the successor case. (Contributed by NM, 19-Sep-2006)

Ref Expression
Hypotheses rankxplim.1 ⊢ A ∈ V
rankxplim.2 ⊢ B ∈ V
Assertion rankxplim ⊢ Lim ⁡ rank ⁡ A ∪ B ∧ A × B ≠ ∅ → rank ⁡ A × B = rank ⁡ A ∪ B

Proof

Step Hyp Ref Expression
1 rankxplim.1 ⊢ A ∈ V
2 rankxplim.2 ⊢ B ∈ V
3 pwuni ⊢ x y ⊆ 𝒫 ⋃ x y
4 vex ⊢ x ∈ V
5 vex ⊢ y ∈ V
6 4 5 uniop ⊢ ⋃ x y = x y
7 6 pweqi ⊢ 𝒫 ⋃ x y = 𝒫 x y
8 3 7 sseqtri ⊢ x y ⊆ 𝒫 x y
9 pwuni ⊢ x y ⊆ 𝒫 ⋃ x y
10 4 5 unipr ⊢ ⋃ x y = x ∪ y
11 10 pweqi ⊢ 𝒫 ⋃ x y = 𝒫 x ∪ y
12 9 11 sseqtri ⊢ x y ⊆ 𝒫 x ∪ y
13 12 sspwi ⊢ 𝒫 x y ⊆ 𝒫 𝒫 x ∪ y
14 8 13 sstri ⊢ x y ⊆ 𝒫 𝒫 x ∪ y
15 4 5 unex ⊢ x ∪ y ∈ V
16 15 pwex ⊢ 𝒫 x ∪ y ∈ V
17 16 pwex ⊢ 𝒫 𝒫 x ∪ y ∈ V
18 17 rankss ⊢ x y ⊆ 𝒫 𝒫 x ∪ y → rank ⁡ x y ⊆ rank ⁡ 𝒫 𝒫 x ∪ y
19 14 18 ax-mp ⊢ rank ⁡ x y ⊆ rank ⁡ 𝒫 𝒫 x ∪ y
20 1 rankel ⊢ x ∈ A → rank ⁡ x ∈ rank ⁡ A
21 2 rankel ⊢ y ∈ B → rank ⁡ y ∈ rank ⁡ B
22 4 5 1 2 rankelun ⊢ rank ⁡ x ∈ rank ⁡ A ∧ rank ⁡ y ∈ rank ⁡ B → rank ⁡ x ∪ y ∈ rank ⁡ A ∪ B
23 20 21 22 syl2an ⊢ x ∈ A ∧ y ∈ B → rank ⁡ x ∪ y ∈ rank ⁡ A ∪ B
24 23 adantl ⊢ Lim ⁡ rank ⁡ A ∪ B ∧ x ∈ A ∧ y ∈ B → rank ⁡ x ∪ y ∈ rank ⁡ A ∪ B
25 ranklim ⊢ Lim ⁡ rank ⁡ A ∪ B → rank ⁡ x ∪ y ∈ rank ⁡ A ∪ B ↔ rank ⁡ 𝒫 x ∪ y ∈ rank ⁡ A ∪ B
26 ranklim ⊢ Lim ⁡ rank ⁡ A ∪ B → rank ⁡ 𝒫 x ∪ y ∈ rank ⁡ A ∪ B ↔ rank ⁡ 𝒫 𝒫 x ∪ y ∈ rank ⁡ A ∪ B
27 25 26 bitrd ⊢ Lim ⁡ rank ⁡ A ∪ B → rank ⁡ x ∪ y ∈ rank ⁡ A ∪ B ↔ rank ⁡ 𝒫 𝒫 x ∪ y ∈ rank ⁡ A ∪ B
28 27 adantr ⊢ Lim ⁡ rank ⁡ A ∪ B ∧ x ∈ A ∧ y ∈ B → rank ⁡ x ∪ y ∈ rank ⁡ A ∪ B ↔ rank ⁡ 𝒫 𝒫 x ∪ y ∈ rank ⁡ A ∪ B
29 24 28 mpbid ⊢ Lim ⁡ rank ⁡ A ∪ B ∧ x ∈ A ∧ y ∈ B → rank ⁡ 𝒫 𝒫 x ∪ y ∈ rank ⁡ A ∪ B
30 rankon ⊢ rank ⁡ x y ∈ On
31 rankon ⊢ rank ⁡ A ∪ B ∈ On
32 ontr2 ⊢ rank ⁡ x y ∈ On ∧ rank ⁡ A ∪ B ∈ On → rank ⁡ x y ⊆ rank ⁡ 𝒫 𝒫 x ∪ y ∧ rank ⁡ 𝒫 𝒫 x ∪ y ∈ rank ⁡ A ∪ B → rank ⁡ x y ∈ rank ⁡ A ∪ B
33 30 31 32 mp2an ⊢ rank ⁡ x y ⊆ rank ⁡ 𝒫 𝒫 x ∪ y ∧ rank ⁡ 𝒫 𝒫 x ∪ y ∈ rank ⁡ A ∪ B → rank ⁡ x y ∈ rank ⁡ A ∪ B
34 19 29 33 sylancr ⊢ Lim ⁡ rank ⁡ A ∪ B ∧ x ∈ A ∧ y ∈ B → rank ⁡ x y ∈ rank ⁡ A ∪ B
35 30 31 onsucssi ⊢ rank ⁡ x y ∈ rank ⁡ A ∪ B ↔ suc ⁡ rank ⁡ x y ⊆ rank ⁡ A ∪ B
36 34 35 sylib ⊢ Lim ⁡ rank ⁡ A ∪ B ∧ x ∈ A ∧ y ∈ B → suc ⁡ rank ⁡ x y ⊆ rank ⁡ A ∪ B
37 36 ralrimivva ⊢ Lim ⁡ rank ⁡ A ∪ B → ∀ x ∈ A ∀ y ∈ B suc ⁡ rank ⁡ x y ⊆ rank ⁡ A ∪ B
38 fveq2 ⊢ z = x y → rank ⁡ z = rank ⁡ x y
39 suceq ⊢ rank ⁡ z = rank ⁡ x y → suc ⁡ rank ⁡ z = suc ⁡ rank ⁡ x y
40 38 39 syl ⊢ z = x y → suc ⁡ rank ⁡ z = suc ⁡ rank ⁡ x y
41 40 sseq1d ⊢ z = x y → suc ⁡ rank ⁡ z ⊆ rank ⁡ A ∪ B ↔ suc ⁡ rank ⁡ x y ⊆ rank ⁡ A ∪ B
42 41 ralxp ⊢ ∀ z ∈ A × B suc ⁡ rank ⁡ z ⊆ rank ⁡ A ∪ B ↔ ∀ x ∈ A ∀ y ∈ B suc ⁡ rank ⁡ x y ⊆ rank ⁡ A ∪ B
43 1 2 xpex ⊢ A × B ∈ V
44 43 rankbnd ⊢ ∀ z ∈ A × B suc ⁡ rank ⁡ z ⊆ rank ⁡ A ∪ B ↔ rank ⁡ A × B ⊆ rank ⁡ A ∪ B
45 42 44 bitr3i ⊢ ∀ x ∈ A ∀ y ∈ B suc ⁡ rank ⁡ x y ⊆ rank ⁡ A ∪ B ↔ rank ⁡ A × B ⊆ rank ⁡ A ∪ B
46 37 45 sylib ⊢ Lim ⁡ rank ⁡ A ∪ B → rank ⁡ A × B ⊆ rank ⁡ A ∪ B
47 46 adantr ⊢ Lim ⁡ rank ⁡ A ∪ B ∧ A × B ≠ ∅ → rank ⁡ A × B ⊆ rank ⁡ A ∪ B
48 1 2 rankxpl ⊢ A × B ≠ ∅ → rank ⁡ A ∪ B ⊆ rank ⁡ A × B
49 48 adantl ⊢ Lim ⁡ rank ⁡ A ∪ B ∧ A × B ≠ ∅ → rank ⁡ A ∪ B ⊆ rank ⁡ A × B
50 47 49 eqssd ⊢ Lim ⁡ rank ⁡ A ∪ B ∧ A × B ≠ ∅ → rank ⁡ A × B = rank ⁡ A ∪ B