Proof of Theorem noseponlem
| Step | Hyp | Ref
| Expression |
| 1 | | nodmon 27695 |
. . . 4
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
| 2 | 1 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → dom 𝐴 ∈ On) |
| 3 | | nodmord 27698 |
. . . . . . 7
⊢ (𝐴 ∈
No → Ord dom 𝐴) |
| 4 | | ordirr 6402 |
. . . . . . 7
⊢ (Ord dom
𝐴 → ¬ dom 𝐴 ∈ dom 𝐴) |
| 5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈
No → ¬ dom 𝐴 ∈ dom 𝐴) |
| 6 | 5 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ dom 𝐴 ∈ dom 𝐴) |
| 7 | | ndmfv 6941 |
. . . . 5
⊢ (¬
dom 𝐴 ∈ dom 𝐴 → (𝐴‘dom 𝐴) = ∅) |
| 8 | 6, 7 | syl 17 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → (𝐴‘dom 𝐴) = ∅) |
| 9 | | nosgnn0 27703 |
. . . . . . 7
⊢ ¬
∅ ∈ {1o, 2o} |
| 10 | | elno3 27700 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
No ↔ (𝐵:dom
𝐵⟶{1o,
2o} ∧ dom 𝐵
∈ On)) |
| 11 | 10 | simplbi 497 |
. . . . . . . . . 10
⊢ (𝐵 ∈
No → 𝐵:dom
𝐵⟶{1o,
2o}) |
| 12 | 11 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → 𝐵:dom 𝐵⟶{1o,
2o}) |
| 13 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → dom 𝐴 ∈ dom 𝐵) |
| 14 | 12, 13 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → (𝐵‘dom 𝐴) ∈ {1o,
2o}) |
| 15 | | eleq1 2829 |
. . . . . . . 8
⊢ ((𝐵‘dom 𝐴) = ∅ → ((𝐵‘dom 𝐴) ∈ {1o, 2o}
↔ ∅ ∈ {1o, 2o})) |
| 16 | 14, 15 | syl5ibcom 245 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → ((𝐵‘dom 𝐴) = ∅ → ∅ ∈
{1o, 2o})) |
| 17 | 9, 16 | mtoi 199 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ (𝐵‘dom 𝐴) = ∅) |
| 18 | 17 | neqned 2947 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → (𝐵‘dom 𝐴) ≠ ∅) |
| 19 | 18 | necomd 2996 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → ∅ ≠ (𝐵‘dom 𝐴)) |
| 20 | 8, 19 | eqnetrd 3008 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → (𝐴‘dom 𝐴) ≠ (𝐵‘dom 𝐴)) |
| 21 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = dom 𝐴 → (𝐴‘𝑥) = (𝐴‘dom 𝐴)) |
| 22 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = dom 𝐴 → (𝐵‘𝑥) = (𝐵‘dom 𝐴)) |
| 23 | 21, 22 | neeq12d 3002 |
. . . 4
⊢ (𝑥 = dom 𝐴 → ((𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ (𝐴‘dom 𝐴) ≠ (𝐵‘dom 𝐴))) |
| 24 | 23 | rspcev 3622 |
. . 3
⊢ ((dom
𝐴 ∈ On ∧ (𝐴‘dom 𝐴) ≠ (𝐵‘dom 𝐴)) → ∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥)) |
| 25 | 2, 20, 24 | syl2anc 584 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → ∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥)) |
| 26 | | df-ne 2941 |
. . . 4
⊢ ((𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 27 | 26 | rexbii 3094 |
. . 3
⊢
(∃𝑥 ∈ On
(𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ∃𝑥 ∈ On ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 28 | | rexnal 3100 |
. . 3
⊢
(∃𝑥 ∈ On
¬ (𝐴‘𝑥) = (𝐵‘𝑥) ↔ ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 29 | 27, 28 | bitri 275 |
. 2
⊢
(∃𝑥 ∈ On
(𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 30 | 25, 29 | sylib 218 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) |