Theorem structcnvcnv

Description: Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Assertion	structcnvcnv	⊢ ( 𝐹 Struct 𝑋 → ◡ ◡ 𝐹 = ( 𝐹 ∖ { ∅ } ) )

Proof

Step	Hyp	Ref	Expression
1		0nelxp	⊢ ¬ ∅ ∈ ( V × V )
2		cnvcnv	⊢ ◡ ◡ 𝐹 = ( 𝐹 ∩ ( V × V ) )
3		inss2	⊢ ( 𝐹 ∩ ( V × V ) ) ⊆ ( V × V )
4	2 3	eqsstri	⊢ ◡ ◡ 𝐹 ⊆ ( V × V )
5	4	sseli	⊢ ( ∅ ∈ ◡ ◡ 𝐹 → ∅ ∈ ( V × V ) )
6	1 5	mto	⊢ ¬ ∅ ∈ ◡ ◡ 𝐹
7		disjsn	⊢ ( ( ◡ ◡ 𝐹 ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ◡ ◡ 𝐹 )
8	6 7	mpbir	⊢ ( ◡ ◡ 𝐹 ∩ { ∅ } ) = ∅
9		cnvcnvss	⊢ ◡ ◡ 𝐹 ⊆ 𝐹
10		reldisj	⊢ ( ◡ ◡ 𝐹 ⊆ 𝐹 → ( ( ◡ ◡ 𝐹 ∩ { ∅ } ) = ∅ ↔ ◡ ◡ 𝐹 ⊆ ( 𝐹 ∖ { ∅ } ) ) )
11	9 10	ax-mp	⊢ ( ( ◡ ◡ 𝐹 ∩ { ∅ } ) = ∅ ↔ ◡ ◡ 𝐹 ⊆ ( 𝐹 ∖ { ∅ } ) )
12	8 11	mpbi	⊢ ◡ ◡ 𝐹 ⊆ ( 𝐹 ∖ { ∅ } )
13	12	a1i	⊢ ( 𝐹 Struct 𝑋 → ◡ ◡ 𝐹 ⊆ ( 𝐹 ∖ { ∅ } ) )
14		structn0fun	⊢ ( 𝐹 Struct 𝑋 → Fun ( 𝐹 ∖ { ∅ } ) )
15		funrel	⊢ ( Fun ( 𝐹 ∖ { ∅ } ) → Rel ( 𝐹 ∖ { ∅ } ) )
16	14 15	syl	⊢ ( 𝐹 Struct 𝑋 → Rel ( 𝐹 ∖ { ∅ } ) )
17		dfrel2	⊢ ( Rel ( 𝐹 ∖ { ∅ } ) ↔ ◡ ◡ ( 𝐹 ∖ { ∅ } ) = ( 𝐹 ∖ { ∅ } ) )
18	16 17	sylib	⊢ ( 𝐹 Struct 𝑋 → ◡ ◡ ( 𝐹 ∖ { ∅ } ) = ( 𝐹 ∖ { ∅ } ) )
19		difss	⊢ ( 𝐹 ∖ { ∅ } ) ⊆ 𝐹
20		cnvss	⊢ ( ( 𝐹 ∖ { ∅ } ) ⊆ 𝐹 → ◡ ( 𝐹 ∖ { ∅ } ) ⊆ ◡ 𝐹 )
21		cnvss	⊢ ( ◡ ( 𝐹 ∖ { ∅ } ) ⊆ ◡ 𝐹 → ◡ ◡ ( 𝐹 ∖ { ∅ } ) ⊆ ◡ ◡ 𝐹 )
22	19 20 21	mp2b	⊢ ◡ ◡ ( 𝐹 ∖ { ∅ } ) ⊆ ◡ ◡ 𝐹
23	18 22	eqsstrrdi	⊢ ( 𝐹 Struct 𝑋 → ( 𝐹 ∖ { ∅ } ) ⊆ ◡ ◡ 𝐹 )
24	13 23	eqssd	⊢ ( 𝐹 Struct 𝑋 → ◡ ◡ 𝐹 = ( 𝐹 ∖ { ∅ } ) )