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 ‘ ∪ 𝐴 ) )