Proof of Theorem sltintdifex
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sltval2 27701 | . 2
⊢ ((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) | 
| 2 |  | fvex 6919 | . . . 4
⊢ (𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V | 
| 3 |  | fvex 6919 | . . . 4
⊢ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V | 
| 4 | 2, 3 | brtp 5528 | . . 3
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o))) | 
| 5 |  | fvprc 6898 | . . . . . . 7
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) | 
| 6 |  | 1n0 8526 | . . . . . . . . 9
⊢
1o ≠ ∅ | 
| 7 | 6 | neii 2942 | . . . . . . . 8
⊢  ¬
1o = ∅ | 
| 8 |  | eqeq1 2741 | . . . . . . . . 9
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ↔ ∅ =
1o)) | 
| 9 |  | eqcom 2744 | . . . . . . . . 9
⊢ (∅
= 1o ↔ 1o = ∅) | 
| 10 | 8, 9 | bitrdi 287 | . . . . . . . 8
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ↔ 1o =
∅)) | 
| 11 | 7, 10 | mtbiri 327 | . . . . . . 7
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o) | 
| 12 | 5, 11 | syl 17 | . . . . . 6
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o) | 
| 13 | 12 | con4i 114 | . . . . 5
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) | 
| 14 | 13 | adantr 480 | . . . 4
⊢ (((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) | 
| 15 | 13 | adantr 480 | . . . 4
⊢ (((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) | 
| 16 |  | fvprc 6898 | . . . . . . 7
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) | 
| 17 |  | 2on0 8522 | . . . . . . . . 9
⊢
2o ≠ ∅ | 
| 18 | 17 | neii 2942 | . . . . . . . 8
⊢  ¬
2o = ∅ | 
| 19 |  | eqeq1 2741 | . . . . . . . . 9
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o ↔ ∅ =
2o)) | 
| 20 |  | eqcom 2744 | . . . . . . . . 9
⊢ (∅
= 2o ↔ 2o = ∅) | 
| 21 | 19, 20 | bitrdi 287 | . . . . . . . 8
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o ↔ 2o =
∅)) | 
| 22 | 18, 21 | mtbiri 327 | . . . . . . 7
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ¬ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) | 
| 23 | 16, 22 | syl 17 | . . . . . 6
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → ¬ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) | 
| 24 | 23 | con4i 114 | . . . . 5
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) | 
| 25 | 24 | adantl 481 | . . . 4
⊢ (((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) | 
| 26 | 14, 15, 25 | 3jaoi 1430 | . . 3
⊢ ((((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o)) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) | 
| 27 | 4, 26 | sylbi 217 | . 2
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) | 
| 28 | 1, 27 | biimtrdi 253 | 1
⊢ ((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No ) → (𝐴 <s 𝐵 → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)) |