Metamath Proof Explorer

Theorem elscott

Description: Membership in a Scott's trick set. (Contributed by BTernaryTau, 3-Jul-2026)

Ref Expression
Assertion elscott ⊢ A ∈ Scott B ↔ A ∈ B ∧ ∀ x ∈ B rank ⁡ A ⊆ rank ⁡ x

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ y = A → rank ⁡ y = rank ⁡ A
2 1 sseq1d ⊢ y = A → rank ⁡ y ⊆ rank ⁡ x ↔ rank ⁡ A ⊆ rank ⁡ x
3 2 ralbidv ⊢ y = A → ∀ x ∈ B rank ⁡ y ⊆ rank ⁡ x ↔ ∀ x ∈ B rank ⁡ A ⊆ rank ⁡ x
4 df-scott ⊢ Scott B = y ∈ B | ∀ x ∈ B rank ⁡ y ⊆ rank ⁡ x
5 3 4 elrab2 ⊢ A ∈ Scott B ↔ A ∈ B ∧ ∀ x ∈ B rank ⁡ A ⊆ rank ⁡ x