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