Proof of Theorem nosepnelem
Step | Hyp | Ref
| Expression |
1 | | sltval2 31809 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
2 | | fvex 6201 |
. . . . 5
⊢ (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ∈ V |
3 | | fvex 6201 |
. . . . 5
⊢ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ∈ V |
4 | 2, 3 | brtp 31639 |
. . . 4
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ (((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
5 | | 1n0 7575 |
. . . . . 6
⊢
1𝑜 ≠ ∅ |
6 | | simpl 473 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜) |
7 | | simpr 477 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) |
8 | 6, 7 | neeq12d 2855 |
. . . . . 6
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ 1𝑜 ≠
∅)) |
9 | 5, 8 | mpbiri 248 |
. . . . 5
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
10 | | df-2o 7561 |
. . . . . . . . . . 11
⊢
2𝑜 = suc 1𝑜 |
11 | | df-1o 7560 |
. . . . . . . . . . 11
⊢
1𝑜 = suc ∅ |
12 | 10, 11 | eqeq12i 2636 |
. . . . . . . . . 10
⊢
(2𝑜 = 1𝑜 ↔ suc
1𝑜 = suc ∅) |
13 | | 1on 7567 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ On |
14 | | 0elon 5778 |
. . . . . . . . . . 11
⊢ ∅
∈ On |
15 | | suc11 5831 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc
1𝑜 = suc ∅ ↔ 1𝑜 =
∅)) |
16 | 13, 14, 15 | mp2an 708 |
. . . . . . . . . 10
⊢ (suc
1𝑜 = suc ∅ ↔ 1𝑜 =
∅) |
17 | 12, 16 | bitri 264 |
. . . . . . . . 9
⊢
(2𝑜 = 1𝑜 ↔
1𝑜 = ∅) |
18 | 17 | necon3bii 2846 |
. . . . . . . 8
⊢
(2𝑜 ≠ 1𝑜 ↔
1𝑜 ≠ ∅) |
19 | 5, 18 | mpbir 221 |
. . . . . . 7
⊢
2𝑜 ≠ 1𝑜 |
20 | 19 | necomi 2848 |
. . . . . 6
⊢
1𝑜 ≠ 2𝑜 |
21 | | simpl 473 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜) |
22 | | simpr 477 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) → (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) |
23 | 21, 22 | neeq12d 2855 |
. . . . . 6
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) → ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ 1𝑜 ≠
2𝑜)) |
24 | 20, 23 | mpbiri 248 |
. . . . 5
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
25 | | 2on 7568 |
. . . . . . . . 9
⊢
2𝑜 ∈ On |
26 | 25 | elexi 3213 |
. . . . . . . 8
⊢
2𝑜 ∈ V |
27 | 26 | prid2 4298 |
. . . . . . 7
⊢
2𝑜 ∈ {1𝑜,
2𝑜} |
28 | 27 | nosgnn0i 31812 |
. . . . . 6
⊢ ∅
≠ 2𝑜 |
29 | | simpl 473 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) |
30 | | simpr 477 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) → (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) |
31 | 29, 30 | neeq12d 2855 |
. . . . . 6
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) → ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ ∅ ≠
2𝑜)) |
32 | 28, 31 | mpbiri 248 |
. . . . 5
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
33 | 9, 24, 32 | 3jaoi 1391 |
. . . 4
⊢ ((((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
34 | 4, 33 | sylbi 207 |
. . 3
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
35 | 1, 34 | syl6bi 243 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
36 | 35 | 3impia 1261 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |