Theorem ndmaovcom

Description: Any operation is commutative outside its domain, analogous to ndmovcom . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypothesis	ndmaov.1	⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
Assertion	ndmaovcom	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → (( 𝐴 𝐹 𝐵 )) = (( 𝐵 𝐹 𝐴 )) )

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
2		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
3	1	eqcomi	⊢ ( 𝑆 × 𝑆 ) = dom 𝐹
4	3	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )
5	2 4	bitr3i	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )
6		ndmaov	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → (( 𝐴 𝐹 𝐵 )) = V )
7	5 6	sylnbi	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → (( 𝐴 𝐹 𝐵 )) = V )
8		ancom	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ↔ ( 𝐵 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) )
9		opelxp	⊢ ( ⟨ 𝐵 , 𝐴 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ( 𝐵 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) )
10	3	eleq2i	⊢ ( ⟨ 𝐵 , 𝐴 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ dom 𝐹 )
11	8 9 10	3bitr2i	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ dom 𝐹 )
12		ndmaov	⊢ ( ¬ ⟨ 𝐵 , 𝐴 ⟩ ∈ dom 𝐹 → (( 𝐵 𝐹 𝐴 )) = V )
13	11 12	sylnbi	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → (( 𝐵 𝐹 𝐴 )) = V )
14	7 13	eqtr4d	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → (( 𝐴 𝐹 𝐵 )) = (( 𝐵 𝐹 𝐴 )) )