Metamath Proof Explorer

Theorem rankc2

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 rankc2 ⊢ ∃ x ∈ A rank ⁡ x = rank ⁡ ⋃ A → rank ⁡ A = suc ⁡ rank ⁡ ⋃ A

Proof

Step Hyp Ref Expression
1 rankr1b.1 ⊢ A ∈ V
2 pwuni ⊢ A ⊆ 𝒫 ⋃ A
3 1 uniex ⊢ ⋃ A ∈ V
4 3 pwex ⊢ 𝒫 ⋃ A ∈ V
5 4 rankss ⊢ A ⊆ 𝒫 ⋃ A → rank ⁡ A ⊆ rank ⁡ 𝒫 ⋃ A
6 2 5 ax-mp ⊢ rank ⁡ A ⊆ rank ⁡ 𝒫 ⋃ A
7 3 rankpw ⊢ rank ⁡ 𝒫 ⋃ A = suc ⁡ rank ⁡ ⋃ A
8 6 7 sseqtri ⊢ rank ⁡ A ⊆ suc ⁡ rank ⁡ ⋃ A
9 8 a1i ⊢ ∃ x ∈ A rank ⁡ x = rank ⁡ ⋃ A → rank ⁡ A ⊆ suc ⁡ rank ⁡ ⋃ A
10 1 rankel ⊢ x ∈ A → rank ⁡ x ∈ rank ⁡ A
11 eleq1 ⊢ rank ⁡ x = rank ⁡ ⋃ A → rank ⁡ x ∈ rank ⁡ A ↔ rank ⁡ ⋃ A ∈ rank ⁡ A
12 10 11 syl5ibcom ⊢ x ∈ A → rank ⁡ x = rank ⁡ ⋃ A → rank ⁡ ⋃ A ∈ rank ⁡ A
13 12 rexlimiv ⊢ ∃ x ∈ A rank ⁡ x = rank ⁡ ⋃ A → rank ⁡ ⋃ A ∈ rank ⁡ A
14 rankon ⊢ rank ⁡ ⋃ A ∈ On
15 rankon ⊢ rank ⁡ A ∈ On
16 14 15 onsucssi ⊢ rank ⁡ ⋃ A ∈ rank ⁡ A ↔ suc ⁡ rank ⁡ ⋃ A ⊆ rank ⁡ A
17 13 16 sylib ⊢ ∃ x ∈ A rank ⁡ x = rank ⁡ ⋃ A → suc ⁡ rank ⁡ ⋃ A ⊆ rank ⁡ A
18 9 17 eqssd ⊢ ∃ x ∈ A rank ⁡ x = rank ⁡ ⋃ A → rank ⁡ A = suc ⁡ rank ⁡ ⋃ A