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

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 ⊢ 𝐴 ∈ V
Assertion rankc1 ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ ( rank ‘ ∪ 𝐴 ) ↔ ( rank ‘ 𝐴 ) = ( rank ‘ ∪ 𝐴 ) )

Proof

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