Proof of Theorem nosepon
| Step | Hyp | Ref
| Expression |
| 1 | | df-ne 2941 |
. . . . . . . 8
⊢ ((𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 2 | 1 | rexbii 3094 |
. . . . . . 7
⊢
(∃𝑥 ∈ On
(𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ∃𝑥 ∈ On ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 3 | 2 | notbii 320 |
. . . . . 6
⊢ (¬
∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ ∃𝑥 ∈ On ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 4 | | dfral2 3099 |
. . . . . 6
⊢
(∀𝑥 ∈ On
(𝐴‘𝑥) = (𝐵‘𝑥) ↔ ¬ ∃𝑥 ∈ On ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 5 | 3, 4 | bitr4i 278 |
. . . . 5
⊢ (¬
∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 6 | | nodmord 27698 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈
No → Ord dom 𝐴) |
| 7 | | nodmord 27698 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈
No → Ord dom 𝐵) |
| 8 | | ordtri3or 6416 |
. . . . . . . . . . . . 13
⊢ ((Ord dom
𝐴 ∧ Ord dom 𝐵) → (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴)) |
| 9 | 6, 7, 8 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴)) |
| 10 | | 3orass 1090 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴) ↔ (dom 𝐴 ∈ dom 𝐵 ∨ (dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
| 11 | | or12 921 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐴 ∈ dom 𝐵 ∨ (dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴)) ↔ (dom 𝐴 = dom 𝐵 ∨ (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
| 12 | 10, 11 | bitri 275 |
. . . . . . . . . . . 12
⊢ ((dom
𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴) ↔ (dom 𝐴 = dom 𝐵 ∨ (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
| 13 | 9, 12 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (dom 𝐴 = dom 𝐵 ∨ (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
| 14 | 13 | ord 865 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ dom 𝐴 = dom 𝐵 → (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
| 15 | | noseponlem 27709 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 16 | 15 | 3expia 1122 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (dom 𝐴 ∈ dom 𝐵 → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
| 17 | | noseponlem 27709 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ∧ dom 𝐵 ∈ dom 𝐴) → ¬ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐴‘𝑥)) |
| 18 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ (𝐵‘𝑥) = (𝐴‘𝑥)) |
| 19 | 18 | ralbii 3093 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈ On
(𝐴‘𝑥) = (𝐵‘𝑥) ↔ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐴‘𝑥)) |
| 20 | 17, 19 | sylnibr 329 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ∧ dom 𝐵 ∈ dom 𝐴) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) |
| 21 | 20 | 3expia 1122 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ) → (dom 𝐵 ∈ dom 𝐴 → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
| 22 | 21 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (dom 𝐵 ∈ dom 𝐴 → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
| 23 | 16, 22 | jaod 860 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
| 24 | 14, 23 | syld 47 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ dom 𝐴 = dom 𝐵 → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
| 25 | 24 | con4d 115 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥) → dom 𝐴 = dom 𝐵)) |
| 26 | 25 | 3impia 1118 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → dom 𝐴 = dom 𝐵) |
| 27 | | ordsson 7803 |
. . . . . . . . . 10
⊢ (Ord dom
𝐴 → dom 𝐴 ⊆ On) |
| 28 | | ssralv 4052 |
. . . . . . . . . 10
⊢ (dom
𝐴 ⊆ On →
(∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥) → ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥))) |
| 29 | 6, 27, 28 | 3syl 18 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → (∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥) → ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥))) |
| 30 | 29 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥) → ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥))) |
| 31 | 30 | 3impia 1118 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) |
| 32 | | nofun 27694 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → Fun 𝐴) |
| 33 | 32 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → Fun 𝐴) |
| 34 | | nofun 27694 |
. . . . . . . . 9
⊢ (𝐵 ∈
No → Fun 𝐵) |
| 35 | 34 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → Fun 𝐵) |
| 36 | | eqfunfv 7056 |
. . . . . . . 8
⊢ ((Fun
𝐴 ∧ Fun 𝐵) → (𝐴 = 𝐵 ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)))) |
| 37 | 33, 35, 36 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → (𝐴 = 𝐵 ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)))) |
| 38 | 26, 31, 37 | mpbir2and 713 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → 𝐴 = 𝐵) |
| 39 | 38 | 3expia 1122 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥) → 𝐴 = 𝐵)) |
| 40 | 5, 39 | biimtrid 242 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ ∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥) → 𝐴 = 𝐵)) |
| 41 | 40 | necon1ad 2957 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥))) |
| 42 | 41 | 3impia 1118 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 ≠ 𝐵) → ∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥)) |
| 43 | | onintrab2 7817 |
. 2
⊢
(∃𝑥 ∈ On
(𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ On) |
| 44 | 42, 43 | sylib 218 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ On) |