Metamath Proof Explorer

Theorem rankxplim2

Description: If the rank of a Cartesian product is a limit ordinal, so is the rank of the union of its arguments. (Contributed by NM, 19-Sep-2006)

Ref Expression
Hypotheses rankxplim.1 ⊢ 𝐴 ∈ V
rankxplim.2 ⊢ 𝐵 ∈ V
Assertion rankxplim2 ( Lim ( rank ‘ ( 𝐴 × 𝐵 ) ) → Lim ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rankxplim.1 ⊢ 𝐴 ∈ V
2 rankxplim.2 ⊢ 𝐵 ∈ V
3 0ellim ⊢ ( Lim ( rank ‘ ( 𝐴 × 𝐵 ) ) → ∅ ∈ ( rank ‘ ( 𝐴 × 𝐵 ) ) )
4 n0i ⊢ ( ∅ ∈ ( rank ‘ ( 𝐴 × 𝐵 ) ) → ¬ ( rank ‘ ( 𝐴 × 𝐵 ) ) = ∅ )
5 3 4 syl ⊢ ( Lim ( rank ‘ ( 𝐴 × 𝐵 ) ) → ¬ ( rank ‘ ( 𝐴 × 𝐵 ) ) = ∅ )
6 df-ne ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ ↔ ¬ ( 𝐴 × 𝐵 ) = ∅ )
7 1 2 xpex ⊢ ( 𝐴 × 𝐵 ) ∈ V
8 7 rankeq0 ⊢ ( ( 𝐴 × 𝐵 ) = ∅ ↔ ( rank ‘ ( 𝐴 × 𝐵 ) ) = ∅ )
9 8 notbii ⊢ ( ¬ ( 𝐴 × 𝐵 ) = ∅ ↔ ¬ ( rank ‘ ( 𝐴 × 𝐵 ) ) = ∅ )
10 6 9 bitr2i ⊢ ( ¬ ( rank ‘ ( 𝐴 × 𝐵 ) ) = ∅ ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
11 5 10 sylib ⊢ ( Lim ( rank ‘ ( 𝐴 × 𝐵 ) ) → ( 𝐴 × 𝐵 ) ≠ ∅ )
12 limuni2 ⊢ ( Lim ( rank ‘ ( 𝐴 × 𝐵 ) ) → Lim ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) )
13 limuni2 ⊢ ( Lim ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) → Lim ∪ ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) )
14 12 13 syl ⊢ ( Lim ( rank ‘ ( 𝐴 × 𝐵 ) ) → Lim ∪ ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) )
15 rankuni ⊢ ( rank ‘ ∪ ∪ ( 𝐴 × 𝐵 ) ) = ∪ ( rank ‘ ∪ ( 𝐴 × 𝐵 ) )
16 rankuni ⊢ ( rank ‘ ∪ ( 𝐴 × 𝐵 ) ) = ∪ ( rank ‘ ( 𝐴 × 𝐵 ) )
17 16 unieqi ⊢ ∪ ( rank ‘ ∪ ( 𝐴 × 𝐵 ) ) = ∪ ∪ ( rank ‘ ( 𝐴 × 𝐵 ) )
18 15 17 eqtr2i ⊢ ∪ ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) = ( rank ‘ ∪ ∪ ( 𝐴 × 𝐵 ) )
19 unixp ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ∪ ∪ ( 𝐴 × 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )
20 19 fveq2d ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( rank ‘ ∪ ∪ ( 𝐴 × 𝐵 ) ) = ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )
21 18 20 syl5eq ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ∪ ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) = ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )
22 limeq ⊢ ( ∪ ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) = ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) → ( Lim ∪ ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) ↔ Lim ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
23 21 22 syl ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( Lim ∪ ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) ↔ Lim ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
24 14 23 syl5ib ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( Lim ( rank ‘ ( 𝐴 × 𝐵 ) ) → Lim ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
25 11 24 mpcom ⊢ ( Lim ( rank ‘ ( 𝐴 × 𝐵 ) ) → Lim ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )