Theorem setsnidel

Description: The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021)

	Ref	Expression
Hypotheses	setsidel.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	setsidel.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	setsidel.r	⊢ 𝑅 = ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ )
	setsnidel.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	setsnidel.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
	setsnidel.s	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑆 )
	setsnidel.n	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
Assertion	setsnidel	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		setsidel.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
2		setsidel.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		setsidel.r	⊢ 𝑅 = ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ )
4		setsnidel.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
5		setsnidel.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
6		setsnidel.s	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑆 )
7		setsnidel.n	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
8	4	elexd	⊢ ( 𝜑 → 𝐶 ∈ V )
9	7	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
10		eldifsn	⊢ ( 𝐶 ∈ ( V ∖ { 𝐴 } ) ↔ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) )
11	8 9 10	sylanbrc	⊢ ( 𝜑 → 𝐶 ∈ ( V ∖ { 𝐴 } ) )
12		opelres	⊢ ( 𝐷 ∈ 𝑌 → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↔ ( 𝐶 ∈ ( V ∖ { 𝐴 } ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑆 ) ) )
13	5 12	syl	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ↔ ( 𝐶 ∈ ( V ∖ { 𝐴 } ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑆 ) ) )
14	11 6 13	mpbir2and	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) )
15		elun1	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
16	14 15	syl	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
17		setsval	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
18	1 2 17	syl2anc	⊢ ( 𝜑 → ( 𝑆 sSet ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
19	3 18	syl5eq	⊢ ( 𝜑 → 𝑅 = ( ( 𝑆 ↾ ( V ∖ { 𝐴 } ) ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
20	16 19	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑅 )