Metamath Proof Explorer

Theorem scottrankeqel

Description: If a member of the input set has the same rank as a member of the Scott's trick set, then it is also a member of the Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026)

Ref Expression
Assertion scottrankeqel ⊢ A ∈ Scott B ∧ C ∈ B ∧ rank ⁡ C = rank ⁡ A → C ∈ Scott B

Proof

Step Hyp Ref Expression
1 elscottrank ⊢ A ∈ Scott B → rank ⁡ A = ⋂ rank B
2 1 3ad2ant1 ⊢ A ∈ Scott B ∧ C ∈ B ∧ rank ⁡ C = rank ⁡ A → rank ⁡ A = ⋂ rank B
3 eqtr ⊢ rank ⁡ C = rank ⁡ A ∧ rank ⁡ A = ⋂ rank B → rank ⁡ C = ⋂ rank B
4 3 3ad2antl3 ⊢ A ∈ Scott B ∧ C ∈ B ∧ rank ⁡ C = rank ⁡ A ∧ rank ⁡ A = ⋂ rank B → rank ⁡ C = ⋂ rank B
5 2 4 mpdan ⊢ A ∈ Scott B ∧ C ∈ B ∧ rank ⁡ C = rank ⁡ A → rank ⁡ C = ⋂ rank B
6 elscott2 ⊢ C ∈ Scott B ↔ C ∈ B ∧ rank ⁡ C = ⋂ rank B
7 6 baib ⊢ C ∈ B → C ∈ Scott B ↔ rank ⁡ C = ⋂ rank B
8 7 3ad2ant2 ⊢ A ∈ Scott B ∧ C ∈ B ∧ rank ⁡ C = rank ⁡ A → C ∈ Scott B ↔ rank ⁡ C = ⋂ rank B
9 5 8 mpbird ⊢ A ∈ Scott B ∧ C ∈ B ∧ rank ⁡ C = rank ⁡ A → C ∈ Scott B