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 ( ( 𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin ) → ( ( 𝐴 ∪ 𝐵 ) ≈ 𝐴 ↔ 𝐴 = 𝐵 ) )

Proof

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