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 |
⊢ (( 𝐴 𝐹 𝐵 )) ∈ 𝑆 |