Theorem scottelrankd

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

	Ref	Expression
Hypotheses	scottelrankd.1	⊢ ( 𝜑 → 𝐵 ∈ Scott 𝐴 )
	scottelrankd.2	⊢ ( 𝜑 → 𝐶 ∈ Scott 𝐴 )
Assertion	scottelrankd	⊢ ( 𝜑 → ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		scottelrankd.1	⊢ ( 𝜑 → 𝐵 ∈ Scott 𝐴 )
2		scottelrankd.2	⊢ ( 𝜑 → 𝐶 ∈ Scott 𝐴 )
3		fveq2	⊢ ( 𝑦 = 𝐶 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝐶 ) )
4	3	sseq2d	⊢ ( 𝑦 = 𝐶 → ( ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐶 ) ) )
5		df-scott	⊢ Scott 𝐴 = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
6	1 5	eleqtrdi	⊢ ( 𝜑 → 𝐵 ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } )
7		fveq2	⊢ ( 𝑥 = 𝐵 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝐵 ) )
8	7	sseq1d	⊢ ( 𝑥 = 𝐵 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝑦 ) ) )
9	8	ralbidv	⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝑦 ) ) )
10	9	elrab	⊢ ( 𝐵 ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ↔ ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝑦 ) ) )
11	6 10	sylib	⊢ ( 𝜑 → ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝑦 ) ) )
12	11	simprd	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝑦 ) )
13	2 5	eleqtrdi	⊢ ( 𝜑 → 𝐶 ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } )
14		elrabi	⊢ ( 𝐶 ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } → 𝐶 ∈ 𝐴 )
15	13 14	syl	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
16	4 12 15	rspcdva	⊢ ( 𝜑 → ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐶 ) )