Metamath Proof Explorer

Theorem rankc1

Description: A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006)

Ref Expression
Hypothesis rankr1b.1 ⊢ A ∈ V
Assertion rankc1 ⊢ ∀ x ∈ A rank ⁡ x ∈ rank ⁡ ⋃ A ↔ rank ⁡ A = rank ⁡ ⋃ A

Proof

Step Hyp Ref Expression
1 rankr1b.1 ⊢ A ∈ V
2 1 rankuniss ⊢ rank ⁡ ⋃ A ⊆ rank ⁡ A
3 2 biantru ⊢ rank ⁡ A ⊆ rank ⁡ ⋃ A ↔ rank ⁡ A ⊆ rank ⁡ ⋃ A ∧ rank ⁡ ⋃ A ⊆ rank ⁡ A
4 iunss ⊢ ⋃ x ∈ A suc ⁡ rank ⁡ x ⊆ rank ⁡ ⋃ A ↔ ∀ x ∈ A suc ⁡ rank ⁡ x ⊆ rank ⁡ ⋃ A
5 1 rankval4 ⊢ rank ⁡ A = ⋃ x ∈ A suc ⁡ rank ⁡ x
6 5 sseq1i ⊢ rank ⁡ A ⊆ rank ⁡ ⋃ A ↔ ⋃ x ∈ A suc ⁡ rank ⁡ x ⊆ rank ⁡ ⋃ A
7 rankon ⊢ rank ⁡ x ∈ On
8 rankon ⊢ rank ⁡ ⋃ A ∈ On
9 7 8 onsucssi ⊢ rank ⁡ x ∈ rank ⁡ ⋃ A ↔ suc ⁡ rank ⁡ x ⊆ rank ⁡ ⋃ A
10 9 ralbii ⊢ ∀ x ∈ A rank ⁡ x ∈ rank ⁡ ⋃ A ↔ ∀ x ∈ A suc ⁡ rank ⁡ x ⊆ rank ⁡ ⋃ A
11 4 6 10 3bitr4ri ⊢ ∀ x ∈ A rank ⁡ x ∈ rank ⁡ ⋃ A ↔ rank ⁡ A ⊆ rank ⁡ ⋃ A
12 eqss ⊢ rank ⁡ A = rank ⁡ ⋃ A ↔ rank ⁡ A ⊆ rank ⁡ ⋃ A ∧ rank ⁡ ⋃ A ⊆ rank ⁡ A
13 3 11 12 3bitr4i ⊢ ∀ x ∈ A rank ⁡ x ∈ rank ⁡ ⋃ A ↔ rank ⁡ A = rank ⁡ ⋃ A