Proof of Theorem findcard2sd
Step | Hyp | Ref
| Expression |
1 | | ssid 3167 |
. 2
⊢ 𝐴 ⊆ 𝐴 |
2 | | findcard2sd.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
3 | 2 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → 𝐴 ∈ Fin) |
4 | | sseq1 3170 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
5 | 4 | anbi2d 461 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝜑 ∧ 𝑥 ⊆ 𝐴) ↔ (𝜑 ∧ ∅ ⊆ 𝐴))) |
6 | | findcard2sd.ch |
. . . . 5
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) |
7 | 5, 6 | imbi12d 233 |
. . . 4
⊢ (𝑥 = ∅ → (((𝜑 ∧ 𝑥 ⊆ 𝐴) → 𝜓) ↔ ((𝜑 ∧ ∅ ⊆ 𝐴) → 𝜒))) |
8 | | sseq1 3170 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
9 | 8 | anbi2d 461 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ⊆ 𝐴) ↔ (𝜑 ∧ 𝑦 ⊆ 𝐴))) |
10 | | findcard2sd.th |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) |
11 | 9, 10 | imbi12d 233 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ⊆ 𝐴) → 𝜓) ↔ ((𝜑 ∧ 𝑦 ⊆ 𝐴) → 𝜃))) |
12 | | sseq1 3170 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) |
13 | 12 | anbi2d 461 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝜑 ∧ 𝑥 ⊆ 𝐴) ↔ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴))) |
14 | | findcard2sd.ta |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏)) |
15 | 13, 14 | imbi12d 233 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((𝜑 ∧ 𝑥 ⊆ 𝐴) → 𝜓) ↔ ((𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → 𝜏))) |
16 | | sseq1 3170 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
17 | 16 | anbi2d 461 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝜑 ∧ 𝑥 ⊆ 𝐴) ↔ (𝜑 ∧ 𝐴 ⊆ 𝐴))) |
18 | | findcard2sd.et |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) |
19 | 17, 18 | imbi12d 233 |
. . . 4
⊢ (𝑥 = 𝐴 → (((𝜑 ∧ 𝑥 ⊆ 𝐴) → 𝜓) ↔ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → 𝜂))) |
20 | | findcard2sd.z |
. . . . 5
⊢ (𝜑 → 𝜒) |
21 | 20 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ ∅ ⊆ 𝐴) → 𝜒) |
22 | | simprl 526 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝜑) |
23 | | simprr 527 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
24 | 23 | unssad 3304 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑦 ⊆ 𝐴) |
25 | 22, 24 | jca 304 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝜑 ∧ 𝑦 ⊆ 𝐴)) |
26 | | simpll 524 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑦 ∈ Fin) |
27 | | id 19 |
. . . . . . . . . . 11
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
28 | | vsnid 3613 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ {𝑧} |
29 | | elun2 3295 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ {𝑧} → 𝑧 ∈ (𝑦 ∪ {𝑧})) |
30 | 28, 29 | mp1i 10 |
. . . . . . . . . . 11
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑧 ∈ (𝑦 ∪ {𝑧})) |
31 | 27, 30 | sseldd 3148 |
. . . . . . . . . 10
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑧 ∈ 𝐴) |
32 | 31 | ad2antll 488 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ 𝐴) |
33 | | simplr 525 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧 ∈ 𝑦) |
34 | 32, 33 | eldifd 3131 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ (𝐴 ∖ 𝑦)) |
35 | | findcard2sd.i |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏)) |
36 | 22, 26, 24, 34, 35 | syl22anc 1234 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝜃 → 𝜏)) |
37 | 25, 36 | embantd 56 |
. . . . . 6
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (((𝜑 ∧ 𝑦 ⊆ 𝐴) → 𝜃) → 𝜏)) |
38 | 37 | ex 114 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (((𝜑 ∧ 𝑦 ⊆ 𝐴) → 𝜃) → 𝜏))) |
39 | 38 | com23 78 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (((𝜑 ∧ 𝑦 ⊆ 𝐴) → 𝜃) → ((𝜑 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → 𝜏))) |
40 | 7, 11, 15, 19, 21, 39 | findcard2s 6865 |
. . 3
⊢ (𝐴 ∈ Fin → ((𝜑 ∧ 𝐴 ⊆ 𝐴) → 𝜂)) |
41 | 3, 40 | mpcom 36 |
. 2
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝐴) → 𝜂) |
42 | 1, 41 | mpan2 423 |
1
⊢ (𝜑 → 𝜂) |