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

Metamath Proof Explorer

Theorem idsset

Description: _I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Assertion idsset I = ( SSet ∩ ◡ SSet )

Proof

Step Hyp Ref Expression
1 reli ⊢ Rel I
2 relsset ⊢ Rel SSet
3 relin1 ⊢ ( Rel SSet → Rel ( SSet ∩ ◡ SSet ) )
4 2 3 ax-mp ⊢ Rel ( SSet ∩ ◡ SSet )
5 eqss ⊢ ( 𝑦 = 𝑧 ↔ ( 𝑦 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
6 vex ⊢ 𝑧 ∈ V
7 6 ideq ⊢ ( 𝑦 I 𝑧 ↔ 𝑦 = 𝑧 )
8 brin ⊢ ( 𝑦 ( SSet ∩ ◡ SSet ) 𝑧 ↔ ( 𝑦 SSet 𝑧 ∧ 𝑦 ◡ SSet 𝑧 ) )
9 6 brsset ⊢ ( 𝑦 SSet 𝑧 ↔ 𝑦 ⊆ 𝑧 )
10 vex ⊢ 𝑦 ∈ V
11 10 6 brcnv ⊢ ( 𝑦 ◡ SSet 𝑧 ↔ 𝑧 SSet 𝑦 )
12 10 brsset ⊢ ( 𝑧 SSet 𝑦 ↔ 𝑧 ⊆ 𝑦 )
13 11 12 bitri ⊢ ( 𝑦 ◡ SSet 𝑧 ↔ 𝑧 ⊆ 𝑦 )
14 9 13 anbi12i ⊢ ( ( 𝑦 SSet 𝑧 ∧ 𝑦 ◡ SSet 𝑧 ) ↔ ( 𝑦 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
15 8 14 bitri ⊢ ( 𝑦 ( SSet ∩ ◡ SSet ) 𝑧 ↔ ( 𝑦 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
16 5 7 15 3bitr4i ⊢ ( 𝑦 I 𝑧 ↔ 𝑦 ( SSet ∩ ◡ SSet ) 𝑧 )
17 1 4 16 eqbrriv ⊢ I = ( SSet ∩ ◡ SSet )