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 ) ) )