Theorem ndmaovcl

Description: The "closure" of an operation outside its domain, when the operation's value is a set in contrast to ndmovcl where it is required that the domain contains the empty set ( (/) e. S ). (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypotheses	ndmaov.1	⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
	ndmaovcl.2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 )
	ndmaovcl.3	⊢ (( 𝐴 𝐹 𝐵 )) ∈ V
Assertion	ndmaovcl	⊢ (( 𝐴 𝐹 𝐵 )) ∈ 𝑆

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
2		ndmaovcl.2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 )
3		ndmaovcl.3	⊢ (( 𝐴 𝐹 𝐵 )) ∈ V
4		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
5	1	eqcomi	⊢ ( 𝑆 × 𝑆 ) = dom 𝐹
6	5	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )
7		ndmaov	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → (( 𝐴 𝐹 𝐵 )) = V )
8		eleq1	⊢ ( (( 𝐴 𝐹 𝐵 )) = V → ( (( 𝐴 𝐹 𝐵 )) ∈ V ↔ V ∈ V ) )
9	8	biimpd	⊢ ( (( 𝐴 𝐹 𝐵 )) = V → ( (( 𝐴 𝐹 𝐵 )) ∈ V → V ∈ V ) )
10		vprc	⊢ ¬ V ∈ V
11	10	pm2.21i	⊢ ( V ∈ V → (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 )
12	9 11	syl6com	⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ V → ( (( 𝐴 𝐹 𝐵 )) = V → (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 ) )
13	3 7 12	mpsyl	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 )
14	6 13	sylnbi	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑆 × 𝑆 ) → (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 )
15	4 14	sylnbir	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 )
16	2 15	pm2.61i	⊢ (( 𝐴 𝐹 𝐵 )) ∈ 𝑆