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 )