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

Metamath Proof Explorer

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 𝑋 → ◡ ◡ 𝐹 = ( 𝐹 ∖ { ∅ } ) )