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 ⊢ 𝐴 ∈ V
rankxplim.2 ⊢ 𝐵 ∈ V
Assertion rankxplim ( ( Lim ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( rank ‘ ( 𝐴 × 𝐵 ) ) = ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )

Proof

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