Proof of Theorem sltintdifex
Step | Hyp | Ref
| Expression |
1 | | sltval2 31809 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
2 | | fvex 6201 |
. . . 4
⊢ (𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V |
3 | | fvex 6201 |
. . . 4
⊢ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V |
4 | 2, 3 | brtp 31639 |
. . 3
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) =
2𝑜))) |
5 | | fvprc 6185 |
. . . . . . 7
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) |
6 | | 1n0 7575 |
. . . . . . . . 9
⊢
1𝑜 ≠ ∅ |
7 | 6 | neii 2796 |
. . . . . . . 8
⊢ ¬
1𝑜 = ∅ |
8 | | eqeq1 2626 |
. . . . . . . . 9
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ↔ ∅ =
1𝑜)) |
9 | | eqcom 2629 |
. . . . . . . . 9
⊢ (∅
= 1𝑜 ↔ 1𝑜 =
∅) |
10 | 8, 9 | syl6bb 276 |
. . . . . . . 8
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ↔
1𝑜 = ∅)) |
11 | 7, 10 | mtbiri 317 |
. . . . . . 7
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜) |
12 | 5, 11 | syl 17 |
. . . . . 6
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜) |
13 | 12 | con4i 113 |
. . . . 5
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
14 | 13 | adantr 481 |
. . . 4
⊢ (((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
15 | 13 | adantr 481 |
. . . 4
⊢ (((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
16 | | fvprc 6185 |
. . . . . . 7
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) |
17 | | 2on0 7569 |
. . . . . . . . 9
⊢
2𝑜 ≠ ∅ |
18 | 17 | neii 2796 |
. . . . . . . 8
⊢ ¬
2𝑜 = ∅ |
19 | | eqeq1 2626 |
. . . . . . . . 9
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜 ↔ ∅ =
2𝑜)) |
20 | | eqcom 2629 |
. . . . . . . . 9
⊢ (∅
= 2𝑜 ↔ 2𝑜 =
∅) |
21 | 19, 20 | syl6bb 276 |
. . . . . . . 8
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ((𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜 ↔
2𝑜 = ∅)) |
22 | 18, 21 | mtbiri 317 |
. . . . . . 7
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ → ¬ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) |
23 | 16, 22 | syl 17 |
. . . . . 6
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → ¬ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) |
24 | 23 | con4i 113 |
. . . . 5
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜 → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
25 | 24 | adantl 482 |
. . . 4
⊢ (((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
26 | 14, 15, 25 | 3jaoi 1391 |
. . 3
⊢ ((((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜)) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
27 | 4, 26 | sylbi 207 |
. 2
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
28 | 1, 27 | syl6bi 243 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)) |