Metamath Proof Explorer

Theorem fiuneneq

Description: Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion fiuneneq ⊢ A ≈ B ∧ A ∈ Fin → A ∪ B ≈ A ↔ A = B

Proof

Step Hyp Ref Expression
1 simp2 ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A ∈ Fin
2 enfi ⊢ A ≈ B → A ∈ Fin ↔ B ∈ Fin
3 2 3ad2ant1 ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A ∈ Fin ↔ B ∈ Fin
4 1 3 mpbid ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → B ∈ Fin
5 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
6 1 4 5 syl2anc ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A ∪ B ∈ Fin
7 ssun1 ⊢ A ⊆ A ∪ B
8 7 a1i ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A ⊆ A ∪ B
9 simp3 ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A ∪ B ≈ A
10 9 ensymd ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A ≈ A ∪ B
11 fisseneq ⊢ A ∪ B ∈ Fin ∧ A ⊆ A ∪ B ∧ A ≈ A ∪ B → A = A ∪ B
12 6 8 10 11 syl3anc ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A = A ∪ B
13 ssun2 ⊢ B ⊆ A ∪ B
14 13 a1i ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → B ⊆ A ∪ B
15 simp1 ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A ≈ B
16 entr ⊢ A ∪ B ≈ A ∧ A ≈ B → A ∪ B ≈ B
17 9 15 16 syl2anc ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A ∪ B ≈ B
18 17 ensymd ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → B ≈ A ∪ B
19 fisseneq ⊢ A ∪ B ∈ Fin ∧ B ⊆ A ∪ B ∧ B ≈ A ∪ B → B = A ∪ B
20 6 14 18 19 syl3anc ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → B = A ∪ B
21 12 20 eqtr4d ⊢ A ≈ B ∧ A ∈ Fin ∧ A ∪ B ≈ A → A = B
22 21 3expia ⊢ A ≈ B ∧ A ∈ Fin → A ∪ B ≈ A → A = B
23 enrefg ⊢ A ∈ Fin → A ≈ A
24 23 adantl ⊢ A ≈ B ∧ A ∈ Fin → A ≈ A
25 unidm ⊢ A ∪ A = A
26 uneq2 ⊢ A = B → A ∪ A = A ∪ B
27 25 26 eqtr3id ⊢ A = B → A = A ∪ B
28 27 breq1d ⊢ A = B → A ≈ A ↔ A ∪ B ≈ A
29 24 28 syl5ibcom ⊢ A ≈ B ∧ A ∈ Fin → A = B → A ∪ B ≈ A
30 22 29 impbid ⊢ A ≈ B ∧ A ∈ Fin → A ∪ B ≈ A ↔ A = B