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

Metamath Proof Explorer

Theorem dfssr2

Description: Alternate definition of the subset relation. (Contributed by Peter Mazsa, 9-Aug-2021)

Ref Expression
Assertion dfssr2 S = ( ( V × V ) ∖ ran ( E ⋉ ( V ∖ E ) ) )

Proof

Step Hyp Ref Expression
1 epel ⊢ ( 𝑧 E 𝑥 ↔ 𝑧 ∈ 𝑥 )
2 brvdif ⊢ ( 𝑧 ( V ∖ E ) 𝑦 ↔ ¬ 𝑧 E 𝑦 )
3 epel ⊢ ( 𝑧 E 𝑦 ↔ 𝑧 ∈ 𝑦 )
4 2 3 xchbinx ⊢ ( 𝑧 ( V ∖ E ) 𝑦 ↔ ¬ 𝑧 ∈ 𝑦 )
5 1 4 anbi12i ⊢ ( ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ 𝑦 ) )
6 5 exbii ⊢ ( ∃ 𝑧 ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ 𝑦 ) )
7 6 notbii ⊢ ( ¬ ∃ 𝑧 ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) ↔ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ 𝑦 ) )
8 dfss6 ⊢ ( 𝑥 ⊆ 𝑦 ↔ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ 𝑦 ) )
9 7 8 bitr4i ⊢ ( ¬ ∃ 𝑧 ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) ↔ 𝑥 ⊆ 𝑦 )
10 9 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ ∃ 𝑧 ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊆ 𝑦 }
11 rnxrn ⊢ ran ( E ⋉ ( V ∖ E ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) }
12 11 difeq2i ⊢ ( ( V × V ) ∖ ran ( E ⋉ ( V ∖ E ) ) ) = ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) } )
13 vvdifopab ⊢ ( ( V × V ) ∖ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ ∃ 𝑧 ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) }
14 12 13 eqtri ⊢ ( ( V × V ) ∖ ran ( E ⋉ ( V ∖ E ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ¬ ∃ 𝑧 ( 𝑧 E 𝑥 ∧ 𝑧 ( V ∖ E ) 𝑦 ) }
15 df-ssr ⊢ S = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊆ 𝑦 }
16 10 14 15 3eqtr4ri ⊢ S = ( ( V × V ) ∖ ran ( E ⋉ ( V ∖ E ) ) )