Proof of Theorem nosepnelem
Step | Hyp | Ref
| Expression |
1 | | sltval2 33867 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
2 | | fvex 6779 |
. . . . 5
⊢ (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ∈ V |
3 | | fvex 6779 |
. . . . 5
⊢ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ∈ V |
4 | 2, 3 | brtp 33725 |
. . . 4
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ (((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o))) |
5 | | 1n0 8305 |
. . . . . 6
⊢
1o ≠ ∅ |
6 | | simpl 483 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o) |
7 | | simpr 485 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) |
8 | 6, 7 | neeq12d 3005 |
. . . . . 6
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ 1o ≠
∅)) |
9 | 5, 8 | mpbiri 257 |
. . . . 5
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
10 | | df-2o 8285 |
. . . . . . . . . . 11
⊢
2o = suc 1o |
11 | | df-1o 8284 |
. . . . . . . . . . 11
⊢
1o = suc ∅ |
12 | 10, 11 | eqeq12i 2756 |
. . . . . . . . . 10
⊢
(2o = 1o ↔ suc 1o = suc
∅) |
13 | | 1on 8296 |
. . . . . . . . . . 11
⊢
1o ∈ On |
14 | | 0elon 6312 |
. . . . . . . . . . 11
⊢ ∅
∈ On |
15 | | suc11 6362 |
. . . . . . . . . . 11
⊢
((1o ∈ On ∧ ∅ ∈ On) → (suc
1o = suc ∅ ↔ 1o = ∅)) |
16 | 13, 14, 15 | mp2an 689 |
. . . . . . . . . 10
⊢ (suc
1o = suc ∅ ↔ 1o = ∅) |
17 | 12, 16 | bitri 274 |
. . . . . . . . 9
⊢
(2o = 1o ↔ 1o =
∅) |
18 | 17 | necon3bii 2996 |
. . . . . . . 8
⊢
(2o ≠ 1o ↔ 1o ≠
∅) |
19 | 5, 18 | mpbir 230 |
. . . . . . 7
⊢
2o ≠ 1o |
20 | 19 | necomi 2998 |
. . . . . 6
⊢
1o ≠ 2o |
21 | | simpl 483 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o) |
22 | | simpr 485 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) |
23 | 21, 22 | neeq12d 3005 |
. . . . . 6
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ 1o ≠
2o)) |
24 | 20, 23 | mpbiri 257 |
. . . . 5
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
25 | | 2on 8298 |
. . . . . . . . 9
⊢
2o ∈ On |
26 | 25 | elexi 3448 |
. . . . . . . 8
⊢
2o ∈ V |
27 | 26 | prid2 4699 |
. . . . . . 7
⊢
2o ∈ {1o, 2o} |
28 | 27 | nosgnn0i 33870 |
. . . . . 6
⊢ ∅
≠ 2o |
29 | | simpl 483 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) |
30 | | simpr 485 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) |
31 | 29, 30 | neeq12d 3005 |
. . . . . 6
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ ∅ ≠
2o)) |
32 | 28, 31 | mpbiri 257 |
. . . . 5
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
33 | 9, 24, 32 | 3jaoi 1426 |
. . . 4
⊢ ((((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o)) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
34 | 4, 33 | sylbi 216 |
. . 3
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
35 | 1, 34 | syl6bi 252 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
36 | 35 | 3impia 1116 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |