This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem setlikespec

Description: If R is set-like in A , then all predecessor classes of elements of A exist. (Contributed by Scott Fenton, 20-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion setlikespec ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )

Proof

Step Hyp Ref Expression
1 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑋 ) }
2 vex ⊢ 𝑥 ∈ V
3 2 elpred ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑥 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑋 ) ) )
4 3 eqabdv ⊢ ( 𝑋 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑋 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑋 ) } )
5 1 4 eqtr4id ⊢ ( 𝑋 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
6 5 adantr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
7 seex ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } ∈ V )
8 7 ancoms ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑋 } ∈ V )
9 6 8 eqeltrrd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )