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 eqtrid ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 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 ‘ ( 𝐴𝐵 ) ) )