Proof of Theorem nosepon
Step | Hyp | Ref
| Expression |
1 | | df-ne 2782 |
. . . . . . . 8
⊢ ((𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
2 | 1 | rexbii 3023 |
. . . . . . 7
⊢
(∃𝑥 ∈ On
(𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ∃𝑥 ∈ On ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
3 | 2 | notbii 309 |
. . . . . 6
⊢ (¬
∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ ∃𝑥 ∈ On ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
4 | | dfral2 2977 |
. . . . . 6
⊢
(∀𝑥 ∈ On
(𝐴‘𝑥) = (𝐵‘𝑥) ↔ ¬ ∃𝑥 ∈ On ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
5 | 3, 4 | bitr4i 266 |
. . . . 5
⊢ (¬
∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) |
6 | | nodmord 31050 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈
No → Ord dom 𝐴) |
7 | | nodmord 31050 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈
No → Ord dom 𝐵) |
8 | | ordtri3or 5672 |
. . . . . . . . . . . . 13
⊢ ((Ord dom
𝐴 ∧ Ord dom 𝐵) → (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴)) |
9 | 6, 7, 8 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴)) |
10 | | 3orass 1034 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴) ↔ (dom 𝐴 ∈ dom 𝐵 ∨ (dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
11 | | or12 544 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐴 ∈ dom 𝐵 ∨ (dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴)) ↔ (dom 𝐴 = dom 𝐵 ∨ (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
12 | 10, 11 | bitri 263 |
. . . . . . . . . . . 12
⊢ ((dom
𝐴 ∈ dom 𝐵 ∨ dom 𝐴 = dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴) ↔ (dom 𝐴 = dom 𝐵 ∨ (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
13 | 9, 12 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (dom 𝐴 = dom 𝐵 ∨ (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
14 | 13 | ord 391 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ dom 𝐴 = dom 𝐵 → (dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴))) |
15 | | noseponlem 31065 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) |
16 | 15 | 3expia 1259 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (dom 𝐴 ∈ dom 𝐵 → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
17 | | noseponlem 31065 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ∧ dom 𝐵 ∈ dom 𝐴) → ¬ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐴‘𝑥)) |
18 | | eqcom 2617 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ (𝐵‘𝑥) = (𝐴‘𝑥)) |
19 | 18 | ralbii 2963 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈ On
(𝐴‘𝑥) = (𝐵‘𝑥) ↔ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐴‘𝑥)) |
20 | 17, 19 | sylnibr 318 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ∧ dom 𝐵 ∈ dom 𝐴) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) |
21 | 20 | 3expia 1259 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ) → (dom 𝐵 ∈ dom 𝐴 → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
22 | 21 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (dom 𝐵 ∈ dom 𝐴 → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
23 | 16, 22 | jaod 394 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((dom 𝐴 ∈ dom 𝐵 ∨ dom 𝐵 ∈ dom 𝐴) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
24 | 14, 23 | syld 46 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ dom 𝐴 = dom 𝐵 → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))) |
25 | 24 | con4d 113 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥) → dom 𝐴 = dom 𝐵)) |
26 | 25 | 3impia 1253 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → dom 𝐴 = dom 𝐵) |
27 | | ordsson 6881 |
. . . . . . . . . 10
⊢ (Ord dom
𝐴 → dom 𝐴 ⊆ On) |
28 | | ssralv 3629 |
. . . . . . . . . 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 1253 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) |
32 | | nofun 31046 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → Fun 𝐴) |
33 | 32 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → Fun 𝐴) |
34 | | nofun 31046 |
. . . . . . . . 9
⊢ (𝐵 ∈
No → Fun 𝐵) |
35 | 34 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → Fun 𝐵) |
36 | | eqfunfv 6224 |
. . . . . . . 8
⊢ ((Fun
𝐴 ∧ Fun 𝐵) → (𝐴 = 𝐵 ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)))) |
37 | 33, 35, 36 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → (𝐴 = 𝐵 ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)))) |
38 | 26, 31, 37 | mpbir2and 959 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) → 𝐴 = 𝐵) |
39 | 38 | 3expia 1259 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥) → 𝐴 = 𝐵)) |
40 | 5, 39 | syl5bi 231 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ ∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥) → 𝐴 = 𝐵)) |
41 | 40 | necon1ad 2799 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥))) |
42 | 41 | 3impia 1253 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 ≠ 𝐵) → ∃𝑥 ∈ On (𝐴‘𝑥) ≠ (𝐵‘𝑥)) |
43 | | onintrab2 6894 |
. 2
⊢
(∃𝑥 ∈ On
(𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ On) |
44 | 42, 43 | sylib 207 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ On) |