Theorem scottrankd

Description: Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypothesis	scottrankd.1	⊢ ( 𝜑 → 𝐵 ∈ Scott 𝐴 )
Assertion	scottrankd	⊢ ( 𝜑 → ( rank ‘ Scott 𝐴 ) = suc ( rank ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		scottrankd.1	⊢ ( 𝜑 → 𝐵 ∈ Scott 𝐴 )
2		scottex2	⊢ Scott 𝐴 ∈ V
3	2	rankval4	⊢ ( rank ‘ Scott 𝐴 ) = ∪ 𝑥 ∈ Scott 𝐴 suc ( rank ‘ 𝑥 )
4	3	a1i	⊢ ( 𝜑 → ( rank ‘ Scott 𝐴 ) = ∪ 𝑥 ∈ Scott 𝐴 suc ( rank ‘ 𝑥 ) )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Scott 𝐴 ) → 𝐵 ∈ Scott 𝐴 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Scott 𝐴 ) → 𝑥 ∈ Scott 𝐴 )
7	5 6	scottelrankd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Scott 𝐴 ) → ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝑥 ) )
8	6 5	scottelrankd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Scott 𝐴 ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐵 ) )
9	7 8	eqssd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Scott 𝐴 ) → ( rank ‘ 𝐵 ) = ( rank ‘ 𝑥 ) )
10	9	suceqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Scott 𝐴 ) → suc ( rank ‘ 𝐵 ) = suc ( rank ‘ 𝑥 ) )
11	10	iuneq2dv	⊢ ( 𝜑 → ∪ 𝑥 ∈ Scott 𝐴 suc ( rank ‘ 𝐵 ) = ∪ 𝑥 ∈ Scott 𝐴 suc ( rank ‘ 𝑥 ) )
12	1	ne0d	⊢ ( 𝜑 → Scott 𝐴 ≠ ∅ )
13		iunconst	⊢ ( Scott 𝐴 ≠ ∅ → ∪ 𝑥 ∈ Scott 𝐴 suc ( rank ‘ 𝐵 ) = suc ( rank ‘ 𝐵 ) )
14	12 13	syl	⊢ ( 𝜑 → ∪ 𝑥 ∈ Scott 𝐴 suc ( rank ‘ 𝐵 ) = suc ( rank ‘ 𝐵 ) )
15	4 11 14	3eqtr2d	⊢ ( 𝜑 → ( rank ‘ Scott 𝐴 ) = suc ( rank ‘ 𝐵 ) )