Proof of Theorem sltsgn2
Step | Hyp | Ref
| Expression |
1 | | sltval2 31053 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}))) |
2 | | fvex 6113 |
. . . 4
⊢ (𝐴‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) ∈ V |
3 | | fvex 6113 |
. . . 4
⊢ (𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) ∈ V |
4 | 2, 3 | brtp 30892 |
. . 3
⊢ ((𝐴‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) ↔ (((𝐴‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 1𝑜 ∧ (𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅) ∨ ((𝐴‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 1𝑜 ∧ (𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∧ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) =
2𝑜))) |
5 | | orc 399 |
. . . . 5
⊢ ((𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ → ((𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) =
2𝑜)) |
6 | 5 | adantl 481 |
. . . 4
⊢ (((𝐴‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 1𝑜 ∧ (𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅) → ((𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) =
2𝑜)) |
7 | | olc 398 |
. . . . 5
⊢ ((𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 2𝑜 → ((𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) =
2𝑜)) |
8 | 7 | adantl 481 |
. . . 4
⊢ (((𝐴‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 1𝑜 ∧ (𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 2𝑜) → ((𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) =
2𝑜)) |
9 | 7 | adantl 481 |
. . . 4
⊢ (((𝐴‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∧ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 2𝑜) → ((𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) =
2𝑜)) |
10 | 6, 8, 9 | 3jaoi 1383 |
. . 3
⊢ ((((𝐴‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 1𝑜 ∧ (𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅) ∨ ((𝐴‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 1𝑜 ∧ (𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∧ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 2𝑜)) → ((𝐵‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) =
2𝑜)) |
11 | 4, 10 | sylbi 206 |
. 2
⊢ ((𝐴‘∩ {𝑘
∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) → ((𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) =
2𝑜)) |
12 | 1, 11 | syl6bi 242 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → ((𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) =
2𝑜))) |