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