Step | Hyp | Ref
| Expression |
1 | | sltval2 27020 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
2 | | fvex 6860 |
. . . . 5
⊢ (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ∈ V |
3 | | fvex 6860 |
. . . . 5
⊢ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ∈ V |
4 | 2, 3 | brtp 5485 |
. . . 4
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ (((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o))) |
5 | | 1n0 8439 |
. . . . . 6
⊢
1o ≠ ∅ |
6 | | simpl 484 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o) |
7 | | simpr 486 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) |
8 | 6, 7 | neeq12d 3006 |
. . . . . 6
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ 1o ≠
∅)) |
9 | 5, 8 | mpbiri 258 |
. . . . 5
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
10 | | df-2o 8418 |
. . . . . . . . . . 11
⊢
2o = suc 1o |
11 | | df-1o 8417 |
. . . . . . . . . . 11
⊢
1o = suc ∅ |
12 | 10, 11 | eqeq12i 2755 |
. . . . . . . . . 10
⊢
(2o = 1o ↔ suc 1o = suc
∅) |
13 | | 1on 8429 |
. . . . . . . . . . 11
⊢
1o ∈ On |
14 | | 0elon 6376 |
. . . . . . . . . . 11
⊢ ∅
∈ On |
15 | | suc11 6429 |
. . . . . . . . . . 11
⊢
((1o ∈ On ∧ ∅ ∈ On) → (suc
1o = suc ∅ ↔ 1o = ∅)) |
16 | 13, 14, 15 | mp2an 691 |
. . . . . . . . . 10
⊢ (suc
1o = suc ∅ ↔ 1o = ∅) |
17 | 12, 16 | bitri 275 |
. . . . . . . . 9
⊢
(2o = 1o ↔ 1o =
∅) |
18 | 17 | necon3bii 2997 |
. . . . . . . 8
⊢
(2o ≠ 1o ↔ 1o ≠
∅) |
19 | 5, 18 | mpbir 230 |
. . . . . . 7
⊢
2o ≠ 1o |
20 | 19 | necomi 2999 |
. . . . . 6
⊢
1o ≠ 2o |
21 | | simpl 484 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o) |
22 | | simpr 486 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) |
23 | 21, 22 | neeq12d 3006 |
. . . . . 6
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ 1o ≠
2o)) |
24 | 20, 23 | mpbiri 258 |
. . . . 5
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
25 | | 2on 8431 |
. . . . . . . . 9
⊢
2o ∈ On |
26 | 25 | elexi 3467 |
. . . . . . . 8
⊢
2o ∈ V |
27 | 26 | prid2 4729 |
. . . . . . 7
⊢
2o ∈ {1o, 2o} |
28 | 27 | nosgnn0i 27023 |
. . . . . 6
⊢ ∅
≠ 2o |
29 | | simpl 484 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) |
30 | | simpr 486 |
. . . . . . 7
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) |
31 | 29, 30 | neeq12d 3006 |
. . . . . 6
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ ∅ ≠
2o)) |
32 | 28, 31 | mpbiri 258 |
. . . . 5
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2o) → (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
33 | 9, 24, 32 | 3jaoi 1428 |
. . . 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 253 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
36 | 35 | 3impia 1118 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |