Metamath Proof Explorer

Theorem rankunb

Description: The rank of the union of two sets. Theorem 15.17(iii) of Monk1 p. 112. (Contributed by Mario Carneiro, 10-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankunb ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ B = rank ⁡ A ∪ rank ⁡ B

Proof

Step Hyp Ref Expression
1 unwf ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On ↔ A ∪ B ∈ ⋃ R1 On
2 rankval3b ⊢ A ∪ B ∈ ⋃ R1 On → rank ⁡ A ∪ B = ⋂ y ∈ On | ∀ x ∈ A ∪ B rank ⁡ x ∈ y
3 1 2 sylbi ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ B = ⋂ y ∈ On | ∀ x ∈ A ∪ B rank ⁡ x ∈ y
4 3 eleq2d ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → x ∈ rank ⁡ A ∪ B ↔ x ∈ ⋂ y ∈ On | ∀ x ∈ A ∪ B rank ⁡ x ∈ y
5 vex ⊢ x ∈ V
6 5 elintrab ⊢ x ∈ ⋂ y ∈ On | ∀ x ∈ A ∪ B rank ⁡ x ∈ y ↔ ∀ y ∈ On ∀ x ∈ A ∪ B rank ⁡ x ∈ y → x ∈ y
7 4 6 bitrdi ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → x ∈ rank ⁡ A ∪ B ↔ ∀ y ∈ On ∀ x ∈ A ∪ B rank ⁡ x ∈ y → x ∈ y
8 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
9 rankelb ⊢ A ∈ ⋃ R1 On → x ∈ A → rank ⁡ x ∈ rank ⁡ A
10 elun1 ⊢ rank ⁡ x ∈ rank ⁡ A → rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B
11 9 10 syl6 ⊢ A ∈ ⋃ R1 On → x ∈ A → rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B
12 rankelb ⊢ B ∈ ⋃ R1 On → x ∈ B → rank ⁡ x ∈ rank ⁡ B
13 elun2 ⊢ rank ⁡ x ∈ rank ⁡ B → rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B
14 12 13 syl6 ⊢ B ∈ ⋃ R1 On → x ∈ B → rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B
15 11 14 jaao ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → x ∈ A ∨ x ∈ B → rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B
16 8 15 biimtrid ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → x ∈ A ∪ B → rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B
17 16 ralrimiv ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → ∀ x ∈ A ∪ B rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B
18 rankon ⊢ rank ⁡ A ∈ On
19 rankon ⊢ rank ⁡ B ∈ On
20 18 19 onun2i ⊢ rank ⁡ A ∪ rank ⁡ B ∈ On
21 eleq2 ⊢ y = rank ⁡ A ∪ rank ⁡ B → rank ⁡ x ∈ y ↔ rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B
22 21 ralbidv ⊢ y = rank ⁡ A ∪ rank ⁡ B → ∀ x ∈ A ∪ B rank ⁡ x ∈ y ↔ ∀ x ∈ A ∪ B rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B
23 eleq2 ⊢ y = rank ⁡ A ∪ rank ⁡ B → x ∈ y ↔ x ∈ rank ⁡ A ∪ rank ⁡ B
24 22 23 imbi12d ⊢ y = rank ⁡ A ∪ rank ⁡ B → ∀ x ∈ A ∪ B rank ⁡ x ∈ y → x ∈ y ↔ ∀ x ∈ A ∪ B rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B → x ∈ rank ⁡ A ∪ rank ⁡ B
25 24 rspcv ⊢ rank ⁡ A ∪ rank ⁡ B ∈ On → ∀ y ∈ On ∀ x ∈ A ∪ B rank ⁡ x ∈ y → x ∈ y → ∀ x ∈ A ∪ B rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B → x ∈ rank ⁡ A ∪ rank ⁡ B
26 20 25 ax-mp ⊢ ∀ y ∈ On ∀ x ∈ A ∪ B rank ⁡ x ∈ y → x ∈ y → ∀ x ∈ A ∪ B rank ⁡ x ∈ rank ⁡ A ∪ rank ⁡ B → x ∈ rank ⁡ A ∪ rank ⁡ B
27 17 26 syl5com ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → ∀ y ∈ On ∀ x ∈ A ∪ B rank ⁡ x ∈ y → x ∈ y → x ∈ rank ⁡ A ∪ rank ⁡ B
28 7 27 sylbid ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → x ∈ rank ⁡ A ∪ B → x ∈ rank ⁡ A ∪ rank ⁡ B
29 28 ssrdv ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ B ⊆ rank ⁡ A ∪ rank ⁡ B
30 ssun1 ⊢ A ⊆ A ∪ B
31 rankssb ⊢ A ∪ B ∈ ⋃ R1 On → A ⊆ A ∪ B → rank ⁡ A ⊆ rank ⁡ A ∪ B
32 30 31 mpi ⊢ A ∪ B ∈ ⋃ R1 On → rank ⁡ A ⊆ rank ⁡ A ∪ B
33 ssun2 ⊢ B ⊆ A ∪ B
34 rankssb ⊢ A ∪ B ∈ ⋃ R1 On → B ⊆ A ∪ B → rank ⁡ B ⊆ rank ⁡ A ∪ B
35 33 34 mpi ⊢ A ∪ B ∈ ⋃ R1 On → rank ⁡ B ⊆ rank ⁡ A ∪ B
36 32 35 unssd ⊢ A ∪ B ∈ ⋃ R1 On → rank ⁡ A ∪ rank ⁡ B ⊆ rank ⁡ A ∪ B
37 1 36 sylbi ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ rank ⁡ B ⊆ rank ⁡ A ∪ B
38 29 37 eqssd ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ B = rank ⁡ A ∪ rank ⁡ B