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

Metamath Proof Explorer

Theorem exse2

Description: Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015)

Ref Expression
Assertion exse2 ( 𝑅 ∈ 𝑉 → 𝑅 Se 𝐴 )

Proof

Step Hyp Ref Expression
1 df-rab ⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) }
2 vex ⊢ 𝑦 ∈ V
3 vex ⊢ 𝑥 ∈ V
4 2 3 breldm ⊢ ( 𝑦 𝑅 𝑥 → 𝑦 ∈ dom 𝑅 )
5 4 adantl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) → 𝑦 ∈ dom 𝑅 )
6 5 abssi ⊢ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) } ⊆ dom 𝑅
7 1 6 eqsstri ⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ⊆ dom 𝑅
8 dmexg ⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
9 ssexg ⊢ ( ( { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ⊆ dom 𝑅 ∧ dom 𝑅 ∈ V ) → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
10 7 8 9 sylancr ⊢ ( 𝑅 ∈ 𝑉 → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
11 10 ralrimivw ⊢ ( 𝑅 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
12 df-se ⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
13 11 12 sylibr ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 Se 𝐴 )