Metamath Proof Explorer

Theorem rankung

Description: The rank of the union of two sets. Closed form of rankun . (Contributed by Scott Fenton, 15-Jul-2015)

Ref Expression
Assertion rankung ⊢ A ∈ V ∧ B ∈ W → rank ⁡ A ∪ B = rank ⁡ A ∪ rank ⁡ B

Proof

Step Hyp Ref Expression
1 uneq1 ⊢ x = A → x ∪ y = A ∪ y
2 1 fveq2d ⊢ x = A → rank ⁡ x ∪ y = rank ⁡ A ∪ y
3 fveq2 ⊢ x = A → rank ⁡ x = rank ⁡ A
4 3 uneq1d ⊢ x = A → rank ⁡ x ∪ rank ⁡ y = rank ⁡ A ∪ rank ⁡ y
5 2 4 eqeq12d ⊢ x = A → rank ⁡ x ∪ y = rank ⁡ x ∪ rank ⁡ y ↔ rank ⁡ A ∪ y = rank ⁡ A ∪ rank ⁡ y
6 uneq2 ⊢ y = B → A ∪ y = A ∪ B
7 6 fveq2d ⊢ y = B → rank ⁡ A ∪ y = rank ⁡ A ∪ B
8 fveq2 ⊢ y = B → rank ⁡ y = rank ⁡ B
9 8 uneq2d ⊢ y = B → rank ⁡ A ∪ rank ⁡ y = rank ⁡ A ∪ rank ⁡ B
10 7 9 eqeq12d ⊢ y = B → rank ⁡ A ∪ y = rank ⁡ A ∪ rank ⁡ y ↔ rank ⁡ A ∪ B = rank ⁡ A ∪ rank ⁡ B
11 vex ⊢ x ∈ V
12 vex ⊢ y ∈ V
13 11 12 rankun ⊢ rank ⁡ x ∪ y = rank ⁡ x ∪ rank ⁡ y
14 5 10 13 vtocl2g ⊢ A ∈ V ∧ B ∈ W → rank ⁡ A ∪ B = rank ⁡ A ∪ rank ⁡ B