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 e. Fin ) -> ( ( A u. B ) ~~ A <-> A = B ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> A e. Fin )
2 enfi 
 |-  ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )
3 2 3ad2ant1 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> ( A e. Fin <-> B e. Fin ) )
4 1 3 mpbid 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> B e. Fin )
5 unfi 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
6 1 4 5 syl2anc 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> ( A u. B ) e. Fin )
7 ssun1 
 |-  A C_ ( A u. B )
8 7 a1i 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> A C_ ( A u. B ) )
9 simp3 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> ( A u. B ) ~~ A )
10 9 ensymd 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> A ~~ ( A u. B ) )
11 fisseneq 
 |-  ( ( ( A u. B ) e. Fin /\ A C_ ( A u. B ) /\ A ~~ ( A u. B ) ) -> A = ( A u. B ) )
12 6 8 10 11 syl3anc 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> A = ( A u. B ) )
13 ssun2 
 |-  B C_ ( A u. B )
14 13 a1i 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> B C_ ( A u. B ) )
15 simp1 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> A ~~ B )
16 entr 
 |-  ( ( ( A u. B ) ~~ A /\ A ~~ B ) -> ( A u. B ) ~~ B )
17 9 15 16 syl2anc 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> ( A u. B ) ~~ B )
18 17 ensymd 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> B ~~ ( A u. B ) )
19 fisseneq 
 |-  ( ( ( A u. B ) e. Fin /\ B C_ ( A u. B ) /\ B ~~ ( A u. B ) ) -> B = ( A u. B ) )
20 6 14 18 19 syl3anc 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> B = ( A u. B ) )
21 12 20 eqtr4d 
 |-  ( ( A ~~ B /\ A e. Fin /\ ( A u. B ) ~~ A ) -> A = B )
22 21 3expia 
 |-  ( ( A ~~ B /\ A e. Fin ) -> ( ( A u. B ) ~~ A -> A = B ) )
23 enrefg 
 |-  ( A e. Fin -> A ~~ A )
24 23 adantl 
 |-  ( ( A ~~ B /\ A e. Fin ) -> A ~~ A )
25 unidm 
 |-  ( A u. A ) = A
26 uneq2 
 |-  ( A = B -> ( A u. A ) = ( A u. B ) )
27 25 26 eqtr3id 
 |-  ( A = B -> A = ( A u. B ) )
28 27 breq1d 
 |-  ( A = B -> ( A ~~ A <-> ( A u. B ) ~~ A ) )
29 24 28 syl5ibcom 
 |-  ( ( A ~~ B /\ A e. Fin ) -> ( A = B -> ( A u. B ) ~~ A ) )
30 22 29 impbid 
 |-  ( ( A ~~ B /\ A e. Fin ) -> ( ( A u. B ) ~~ A <-> A = B ) )