Step | Hyp | Ref
| Expression |
1 | | difeq2 4007 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ∖ 𝑥) = (𝐴 ∖ ∅)) |
2 | | dif0 4261 |
. . . . . 6
⊢ (𝐴 ∖ ∅) = 𝐴 |
3 | 1, 2 | eqtrdi 2789 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 ∖ 𝑥) = 𝐴) |
4 | 3 | breq1d 5040 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐴 ∖ 𝑥) ≈ 𝐴 ↔ 𝐴 ≈ 𝐴)) |
5 | 4 | imbi2d 344 |
. . 3
⊢ (𝑥 = ∅ → ((ω
≼ 𝐴 → (𝐴 ∖ 𝑥) ≈ 𝐴) ↔ (ω ≼ 𝐴 → 𝐴 ≈ 𝐴))) |
6 | | difeq2 4007 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑦)) |
7 | 6 | breq1d 5040 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 ∖ 𝑥) ≈ 𝐴 ↔ (𝐴 ∖ 𝑦) ≈ 𝐴)) |
8 | 7 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝑦 → ((ω ≼ 𝐴 → (𝐴 ∖ 𝑥) ≈ 𝐴) ↔ (ω ≼ 𝐴 → (𝐴 ∖ 𝑦) ≈ 𝐴))) |
9 | | difeq2 4007 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝑦 ∪ {𝑧}))) |
10 | | difun1 4180 |
. . . . . 6
⊢ (𝐴 ∖ (𝑦 ∪ {𝑧})) = ((𝐴 ∖ 𝑦) ∖ {𝑧}) |
11 | 9, 10 | eqtrdi 2789 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ∖ 𝑥) = ((𝐴 ∖ 𝑦) ∖ {𝑧})) |
12 | 11 | breq1d 5040 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∖ 𝑥) ≈ 𝐴 ↔ ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴)) |
13 | 12 | imbi2d 344 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((ω ≼ 𝐴 → (𝐴 ∖ 𝑥) ≈ 𝐴) ↔ (ω ≼ 𝐴 → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴))) |
14 | | difeq2 4007 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝐵)) |
15 | 14 | breq1d 5040 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐴 ∖ 𝑥) ≈ 𝐴 ↔ (𝐴 ∖ 𝐵) ≈ 𝐴)) |
16 | 15 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝐵 → ((ω ≼ 𝐴 → (𝐴 ∖ 𝑥) ≈ 𝐴) ↔ (ω ≼ 𝐴 → (𝐴 ∖ 𝐵) ≈ 𝐴))) |
17 | | reldom 8561 |
. . . . 5
⊢ Rel
≼ |
18 | 17 | brrelex2i 5580 |
. . . 4
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) |
19 | | enrefg 8587 |
. . . 4
⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (ω
≼ 𝐴 → 𝐴 ≈ 𝐴) |
21 | | domen2 8710 |
. . . . . . . . 9
⊢ ((𝐴 ∖ 𝑦) ≈ 𝐴 → (ω ≼ (𝐴 ∖ 𝑦) ↔ ω ≼ 𝐴)) |
22 | 21 | biimparc 483 |
. . . . . . . 8
⊢ ((ω
≼ 𝐴 ∧ (𝐴 ∖ 𝑦) ≈ 𝐴) → ω ≼ (𝐴 ∖ 𝑦)) |
23 | | infdifsn 9193 |
. . . . . . . 8
⊢ (ω
≼ (𝐴 ∖ 𝑦) → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ (𝐴 ∖ 𝑦)) |
24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ ((ω
≼ 𝐴 ∧ (𝐴 ∖ 𝑦) ≈ 𝐴) → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ (𝐴 ∖ 𝑦)) |
25 | | entr 8607 |
. . . . . . 7
⊢ ((((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ (𝐴 ∖ 𝑦) ∧ (𝐴 ∖ 𝑦) ≈ 𝐴) → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴) |
26 | 24, 25 | sylancom 591 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ (𝐴 ∖ 𝑦) ≈ 𝐴) → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴) |
27 | 26 | ex 416 |
. . . . 5
⊢ (ω
≼ 𝐴 → ((𝐴 ∖ 𝑦) ≈ 𝐴 → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴)) |
28 | 27 | a2i 14 |
. . . 4
⊢ ((ω
≼ 𝐴 → (𝐴 ∖ 𝑦) ≈ 𝐴) → (ω ≼ 𝐴 → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴)) |
29 | 28 | a1i 11 |
. . 3
⊢ (𝑦 ∈ Fin → ((ω
≼ 𝐴 → (𝐴 ∖ 𝑦) ≈ 𝐴) → (ω ≼ 𝐴 → ((𝐴 ∖ 𝑦) ∖ {𝑧}) ≈ 𝐴))) |
30 | 5, 8, 13, 16, 20, 29 | findcard2 8763 |
. 2
⊢ (𝐵 ∈ Fin → (ω
≼ 𝐴 → (𝐴 ∖ 𝐵) ≈ 𝐴)) |
31 | 30 | impcom 411 |
1
⊢ ((ω
≼ 𝐴 ∧ 𝐵 ∈ Fin) → (𝐴 ∖ 𝐵) ≈ 𝐴) |