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