Proof of Theorem ndmaovass
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ndmaov.1 | . . . . . 6
⊢ dom 𝐹 = (𝑆 × 𝑆) | 
| 2 | 1 | eleq2i 2832 | . . . . 5
⊢ (〈
((𝐴𝐹𝐵)) , 𝐶〉 ∈ dom 𝐹 ↔ 〈 ((𝐴𝐹𝐵)) , 𝐶〉 ∈ (𝑆 × 𝑆)) | 
| 3 |  | opelxp 5720 | . . . . 5
⊢ (〈
((𝐴𝐹𝐵)) , 𝐶〉 ∈ (𝑆 × 𝑆) ↔ ( ((𝐴𝐹𝐵)) ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) | 
| 4 | 2, 3 | bitri 275 | . . . 4
⊢ (〈
((𝐴𝐹𝐵)) , 𝐶〉 ∈ dom 𝐹 ↔ ( ((𝐴𝐹𝐵)) ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) | 
| 5 |  | aovvdm 47202 | . . . . . 6
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝑆 → 〈𝐴, 𝐵〉 ∈ dom 𝐹) | 
| 6 | 1 | eleq2i 2832 | . . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ dom 𝐹 ↔ 〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆)) | 
| 7 |  | opelxp 5720 | . . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) | 
| 8 | 6, 7 | bitri 275 | . . . . . . 7
⊢
(〈𝐴, 𝐵〉 ∈ dom 𝐹 ↔ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) | 
| 9 |  | df-3an 1088 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ↔ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑆)) | 
| 10 | 9 | simplbi2 500 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐶 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) | 
| 11 | 8, 10 | sylbi 217 | . . . . . 6
⊢
(〈𝐴, 𝐵〉 ∈ dom 𝐹 → (𝐶 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) | 
| 12 | 5, 11 | syl 17 | . . . . 5
⊢ ( ((𝐴𝐹𝐵)) ∈ 𝑆 → (𝐶 ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) | 
| 13 | 12 | imp 406 | . . . 4
⊢ ((
((𝐴𝐹𝐵)) ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) | 
| 14 | 4, 13 | sylbi 217 | . . 3
⊢ (〈
((𝐴𝐹𝐵)) , 𝐶〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) | 
| 15 |  | ndmaov 47200 | . . 3
⊢ (¬
〈 ((𝐴𝐹𝐵)) , 𝐶〉 ∈ dom 𝐹 → (( ((𝐴𝐹𝐵)) 𝐹𝐶)) = V) | 
| 16 | 14, 15 | nsyl5 159 | . 2
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (( ((𝐴𝐹𝐵)) 𝐹𝐶)) = V) | 
| 17 | 1 | eleq2i 2832 | . . . . . 6
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 ↔ 〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ (𝑆 × 𝑆)) | 
| 18 |  | opelxp 5720 | . . . . . 6
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ (𝑆 × 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆)) | 
| 19 | 17, 18 | bitri 275 | . . . . 5
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 ↔ (𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆)) | 
| 20 |  | aovvdm 47202 | . . . . . . 7
⊢ ( ((𝐵𝐹𝐶)) ∈ 𝑆 → 〈𝐵, 𝐶〉 ∈ dom 𝐹) | 
| 21 | 1 | eleq2i 2832 | . . . . . . . . 9
⊢
(〈𝐵, 𝐶〉 ∈ dom 𝐹 ↔ 〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑆)) | 
| 22 |  | opelxp 5720 | . . . . . . . . 9
⊢
(〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑆) ↔ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) | 
| 23 | 21, 22 | bitri 275 | . . . . . . . 8
⊢
(〈𝐵, 𝐶〉 ∈ dom 𝐹 ↔ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) | 
| 24 |  | 3anass 1094 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ↔ (𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) | 
| 25 | 24 | biimpri 228 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) | 
| 26 | 25 | a1d 25 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) | 
| 27 | 26 | expcom 413 | . . . . . . . 8
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ∈ 𝑆 → (〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))) | 
| 28 | 23, 27 | sylbi 217 | . . . . . . 7
⊢
(〈𝐵, 𝐶〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 → (〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))) | 
| 29 | 20, 28 | syl 17 | . . . . . 6
⊢ ( ((𝐵𝐹𝐶)) ∈ 𝑆 → (𝐴 ∈ 𝑆 → (〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))) | 
| 30 | 29 | impcom 407 | . . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ ((𝐵𝐹𝐶)) ∈ 𝑆) → (〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) | 
| 31 | 19, 30 | sylbi 217 | . . . 4
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 → (〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))) | 
| 32 | 31 | pm2.43i 52 | . . 3
⊢
(〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) | 
| 33 |  | ndmaov 47200 | . . 3
⊢ (¬
〈𝐴, ((𝐵𝐹𝐶)) 〉 ∈ dom 𝐹 → ((𝐴𝐹 ((𝐵𝐹𝐶)) )) = V) | 
| 34 | 32, 33 | nsyl5 159 | . 2
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝐹 ((𝐵𝐹𝐶)) )) = V) | 
| 35 | 16, 34 | eqtr4d 2779 | 1
⊢ (¬
(𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (( ((𝐴𝐹𝐵)) 𝐹𝐶)) = ((𝐴𝐹 ((𝐵𝐹𝐶)) )) ) |