This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ V
Assertion rankc2 ( ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ ∪ 𝐴 ) → ( rank ‘ 𝐴 ) = suc ( rank ‘ ∪ 𝐴 ) )

Proof

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