Proof of Theorem fiuneneq
| Step | Hyp | Ref
| Expression |
| 1 | | simp2 1138 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐴 ∈ Fin) |
| 2 | | enfi 9227 |
. . . . . . . 8
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) |
| 3 | 2 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) |
| 4 | 1, 3 | mpbid 232 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐵 ∈ Fin) |
| 5 | | unfi 9211 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin) |
| 6 | 1, 4, 5 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → (𝐴 ∪ 𝐵) ∈ Fin) |
| 7 | | ssun1 4178 |
. . . . . 6
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
| 8 | 7 | a1i 11 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐴 ⊆ (𝐴 ∪ 𝐵)) |
| 9 | | simp3 1139 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐴) |
| 10 | 9 | ensymd 9045 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐴 ≈ (𝐴 ∪ 𝐵)) |
| 11 | | fisseneq 9293 |
. . . . 5
⊢ (((𝐴 ∪ 𝐵) ∈ Fin ∧ 𝐴 ⊆ (𝐴 ∪ 𝐵) ∧ 𝐴 ≈ (𝐴 ∪ 𝐵)) → 𝐴 = (𝐴 ∪ 𝐵)) |
| 12 | 6, 8, 10, 11 | syl3anc 1373 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐴 = (𝐴 ∪ 𝐵)) |
| 13 | | ssun2 4179 |
. . . . . 6
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
| 14 | 13 | a1i 11 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐵 ⊆ (𝐴 ∪ 𝐵)) |
| 15 | | simp1 1137 |
. . . . . . 7
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐴 ≈ 𝐵) |
| 16 | | entr 9046 |
. . . . . . 7
⊢ (((𝐴 ∪ 𝐵) ≈ 𝐴 ∧ 𝐴 ≈ 𝐵) → (𝐴 ∪ 𝐵) ≈ 𝐵) |
| 17 | 9, 15, 16 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐵) |
| 18 | 17 | ensymd 9045 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐵 ≈ (𝐴 ∪ 𝐵)) |
| 19 | | fisseneq 9293 |
. . . . 5
⊢ (((𝐴 ∪ 𝐵) ∈ Fin ∧ 𝐵 ⊆ (𝐴 ∪ 𝐵) ∧ 𝐵 ≈ (𝐴 ∪ 𝐵)) → 𝐵 = (𝐴 ∪ 𝐵)) |
| 20 | 6, 14, 18, 19 | syl3anc 1373 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐵 = (𝐴 ∪ 𝐵)) |
| 21 | 12, 20 | eqtr4d 2780 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ∧ (𝐴 ∪ 𝐵) ≈ 𝐴) → 𝐴 = 𝐵) |
| 22 | 21 | 3expia 1122 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin) → ((𝐴 ∪ 𝐵) ≈ 𝐴 → 𝐴 = 𝐵)) |
| 23 | | enrefg 9024 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝐴 ≈ 𝐴) |
| 24 | 23 | adantl 481 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin) → 𝐴 ≈ 𝐴) |
| 25 | | unidm 4157 |
. . . . 5
⊢ (𝐴 ∪ 𝐴) = 𝐴 |
| 26 | | uneq2 4162 |
. . . . 5
⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐴) = (𝐴 ∪ 𝐵)) |
| 27 | 25, 26 | eqtr3id 2791 |
. . . 4
⊢ (𝐴 = 𝐵 → 𝐴 = (𝐴 ∪ 𝐵)) |
| 28 | 27 | breq1d 5153 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐴 ≈ 𝐴 ↔ (𝐴 ∪ 𝐵) ≈ 𝐴)) |
| 29 | 24, 28 | syl5ibcom 245 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin) → (𝐴 = 𝐵 → (𝐴 ∪ 𝐵) ≈ 𝐴)) |
| 30 | 22, 29 | impbid 212 |
1
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin) → ((𝐴 ∪ 𝐵) ≈ 𝐴 ↔ 𝐴 = 𝐵)) |