Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝐴 = ∅) → 𝐴 = ∅) |
2 | | eldifi 3242 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴) |
3 | | ne0i 3413 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) |
4 | 2, 3 | syl 14 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝐴 ≠ ∅) |
5 | 4 | neneqd 2355 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝐴 = ∅) |
6 | 5 | ad2antlr 481 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝐴 = ∅) → ¬ 𝐴 = ∅) |
7 | 1, 6 | pm2.21dd 610 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝐴 = ∅) → ¬ 𝐴 ≈ 𝐵) |
8 | | php5dom 6823 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω → ¬ suc
𝑦 ≼ 𝑦) |
9 | 8 | ad2antlr 481 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → ¬ suc 𝑦 ≼ 𝑦) |
10 | | simplr 520 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → 𝐴 = suc 𝑦) |
11 | | simpr 109 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → 𝐴 ≈ 𝐵) |
12 | | vex 2727 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
13 | 12 | sucex 4473 |
. . . . . . . . . . . . . . 15
⊢ suc 𝑦 ∈ V |
14 | | difss 3246 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑦 ∖ {𝑥}) ⊆ suc 𝑦 |
15 | 13, 14 | ssexi 4117 |
. . . . . . . . . . . . . 14
⊢ (suc
𝑦 ∖ {𝑥}) ∈ V |
16 | | eldifn 3243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵) |
17 | 16 | ad3antlr 485 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → ¬ 𝑥 ∈ 𝐵) |
18 | | simpllr 524 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) → 𝐵 ⊆ 𝐴) |
19 | 18 | adantr 274 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ⊆ 𝐴) |
20 | | simpr 109 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐴 = suc 𝑦) |
21 | 19, 20 | sseqtrd 3178 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ⊆ suc 𝑦) |
22 | | ssdif 3255 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ⊆ suc 𝑦 → (𝐵 ∖ {𝑥}) ⊆ (suc 𝑦 ∖ {𝑥})) |
23 | | disjsn 3635 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ 𝐵) |
24 | | disj3 3459 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∩ {𝑥}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑥})) |
25 | 23, 24 | bitr3i 185 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 ∈ 𝐵 ↔ 𝐵 = (𝐵 ∖ {𝑥})) |
26 | | sseq1 3163 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 = (𝐵 ∖ {𝑥}) → (𝐵 ⊆ (suc 𝑦 ∖ {𝑥}) ↔ (𝐵 ∖ {𝑥}) ⊆ (suc 𝑦 ∖ {𝑥}))) |
27 | 25, 26 | sylbi 120 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ∈ 𝐵 → (𝐵 ⊆ (suc 𝑦 ∖ {𝑥}) ↔ (𝐵 ∖ {𝑥}) ⊆ (suc 𝑦 ∖ {𝑥}))) |
28 | 22, 27 | syl5ibr 155 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑥 ∈ 𝐵 → (𝐵 ⊆ suc 𝑦 → 𝐵 ⊆ (suc 𝑦 ∖ {𝑥}))) |
29 | 17, 21, 28 | sylc 62 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ⊆ (suc 𝑦 ∖ {𝑥})) |
30 | | ssdomg 6738 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑦 ∖ {𝑥}) ∈ V → (𝐵 ⊆ (suc 𝑦 ∖ {𝑥}) → 𝐵 ≼ (suc 𝑦 ∖ {𝑥}))) |
31 | 15, 29, 30 | mpsyl 65 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ≼ (suc 𝑦 ∖ {𝑥})) |
32 | | simplr 520 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝑦 ∈ ω) |
33 | 2 | ad3antlr 485 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝑥 ∈ 𝐴) |
34 | 33, 20 | eleqtrd 2243 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝑥 ∈ suc 𝑦) |
35 | | phplem3g 6816 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ω ∧ 𝑥 ∈ suc 𝑦) → 𝑦 ≈ (suc 𝑦 ∖ {𝑥})) |
36 | 35 | ensymd 6743 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ω ∧ 𝑥 ∈ suc 𝑦) → (suc 𝑦 ∖ {𝑥}) ≈ 𝑦) |
37 | 32, 34, 36 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → (suc 𝑦 ∖ {𝑥}) ≈ 𝑦) |
38 | | domentr 6751 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ≼ (suc 𝑦 ∖ {𝑥}) ∧ (suc 𝑦 ∖ {𝑥}) ≈ 𝑦) → 𝐵 ≼ 𝑦) |
39 | 31, 37, 38 | syl2anc 409 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ≼ 𝑦) |
40 | 39 | adantr 274 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → 𝐵 ≼ 𝑦) |
41 | | endomtr 6750 |
. . . . . . . . . . 11
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝑦) → 𝐴 ≼ 𝑦) |
42 | 11, 40, 41 | syl2anc 409 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → 𝐴 ≼ 𝑦) |
43 | 10, 42 | eqbrtrrd 4003 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴 ≈ 𝐵) → suc 𝑦 ≼ 𝑦) |
44 | 9, 43 | mtand 655 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ω ∧ 𝐵 ⊆
𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → ¬ 𝐴 ≈ 𝐵) |
45 | 44 | ex 114 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ ω) → (𝐴 = suc 𝑦 → ¬ 𝐴 ≈ 𝐵)) |
46 | 45 | rexlimdva 2581 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → (∃𝑦 ∈ ω 𝐴 = suc 𝑦 → ¬ 𝐴 ≈ 𝐵)) |
47 | 46 | imp 123 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) ∧ ∃𝑦 ∈ ω 𝐴 = suc 𝑦) → ¬ 𝐴 ≈ 𝐵) |
48 | | nn0suc 4578 |
. . . . . 6
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑦 ∈ ω 𝐴 = suc 𝑦)) |
49 | 48 | ad2antrr 480 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → (𝐴 = ∅ ∨ ∃𝑦 ∈ ω 𝐴 = suc 𝑦)) |
50 | 7, 47, 49 | mpjaodan 788 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ 𝐵)) → ¬ 𝐴 ≈ 𝐵) |
51 | 50 | ex 114 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝐴 ≈ 𝐵)) |
52 | 51 | exlimdv 1806 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝐴 ≈ 𝐵)) |
53 | 52 | 3impia 1189 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴 ∧ ∃𝑥 𝑥 ∈ (𝐴 ∖ 𝐵)) → ¬ 𝐴 ≈ 𝐵) |