Proof of Theorem nosepne
| Step | Hyp | Ref
| Expression |
| 1 | | sltso 27721 |
. . . 4
⊢ <s Or
No |
| 2 | | sotrine 5632 |
. . . 4
⊢ (( <s
Or No ∧ (𝐴 ∈ No
∧ 𝐵 ∈ No )) → (𝐴 ≠ 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴))) |
| 3 | 1, 2 | mpan 690 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 ≠ 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴))) |
| 4 | | nosepnelem 27724 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
| 5 | 4 | 3expia 1122 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
| 6 | | nosepnelem 27724 |
. . . . . . 7
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ∧ 𝐵 <s 𝐴) → (𝐵‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) ≠ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)})) |
| 7 | | necom 2994 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ (𝐵‘𝑥) ≠ (𝐴‘𝑥)) |
| 8 | 7 | rabbii 3442 |
. . . . . . . . . . 11
⊢ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} = {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)} |
| 9 | 8 | inteqi 4950 |
. . . . . . . . . 10
⊢ ∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} = ∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)} |
| 10 | 9 | fveq2i 6909 |
. . . . . . . . 9
⊢ (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = (𝐴‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) |
| 11 | 9 | fveq2i 6909 |
. . . . . . . . 9
⊢ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = (𝐵‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) |
| 12 | 10, 11 | neeq12i 3007 |
. . . . . . . 8
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)})) |
| 13 | | necom 2994 |
. . . . . . . 8
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) ↔ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) ≠ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)})) |
| 14 | 12, 13 | bitri 275 |
. . . . . . 7
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) ≠ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)})) |
| 15 | 6, 14 | sylibr 234 |
. . . . . 6
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ∧ 𝐵 <s 𝐴) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |
| 16 | 15 | 3expia 1122 |
. . . . 5
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ) → (𝐵 <s 𝐴 → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
| 17 | 16 | ancoms 458 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐵 <s 𝐴 → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
| 18 | 5, 17 | jaod 860 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
| 19 | 3, 18 | sylbid 240 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 ≠ 𝐵 → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
| 20 | 19 | 3impia 1118 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 ≠ 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) |