Metamath Proof Explorer

Theorem rankidb

Description: Identity law for the rank function. (Contributed by NM, 3-Oct-2003) (Revised by Mario Carneiro, 22-Mar-2013)

Ref Expression
Assertion rankidb ⊢ A ∈ ⋃ R1 On → A ∈ R1 ⁡ suc ⁡ rank ⁡ A

Proof

Step Hyp Ref Expression
1 rankwflemb ⊢ A ∈ ⋃ R1 On ↔ ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x
2 nfcv ⊢ Ⅎ _ x R1
3 nfrab1 ⊢ Ⅎ _ x x ∈ On | A ∈ R1 ⁡ suc ⁡ x
4 3 nfint ⊢ Ⅎ _ x ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
5 4 nfsuc ⊢ Ⅎ _ x suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
6 2 5 nffv ⊢ Ⅎ _ x R1 ⁡ suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
7 6 nfel2 ⊢ Ⅎ x A ∈ R1 ⁡ suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
8 suceq ⊢ x = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x → suc ⁡ x = suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
9 8 fveq2d ⊢ x = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x → R1 ⁡ suc ⁡ x = R1 ⁡ suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
10 9 eleq2d ⊢ x = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x → A ∈ R1 ⁡ suc ⁡ x ↔ A ∈ R1 ⁡ suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
11 7 10 onminsb ⊢ ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x → A ∈ R1 ⁡ suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
12 1 11 sylbi ⊢ A ∈ ⋃ R1 On → A ∈ R1 ⁡ suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
13 rankvalb ⊢ A ∈ ⋃ R1 On → rank ⁡ A = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
14 suceq ⊢ rank ⁡ A = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x → suc ⁡ rank ⁡ A = suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
15 13 14 syl ⊢ A ∈ ⋃ R1 On → suc ⁡ rank ⁡ A = suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
16 15 fveq2d ⊢ A ∈ ⋃ R1 On → R1 ⁡ suc ⁡ rank ⁡ A = R1 ⁡ suc ⁡ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
17 12 16 eleqtrrd ⊢ A ∈ ⋃ R1 On → A ∈ R1 ⁡ suc ⁡ rank ⁡ A