Metamath Proof Explorer

Theorem unen

Description: Equinumerosity of union of disjoint sets. Theorem 4 of Suppes p. 92. (Contributed by NM, 11-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion unen 
|- ( ( ( A ~~ B /\ C ~~ D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( A u. C ) ~~ ( B u. D ) )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( A ~~ B <-> E. x x : A -1-1-onto-> B )
2 bren 
 |-  ( C ~~ D <-> E. y y : C -1-1-onto-> D )
3 exdistrv 
 |-  ( E. x E. y ( x : A -1-1-onto-> B /\ y : C -1-1-onto-> D ) <-> ( E. x x : A -1-1-onto-> B /\ E. y y : C -1-1-onto-> D ) )
4 vex 
 |-  x e. _V
5 vex 
 |-  y e. _V
6 4 5 unex 
 |-  ( x u. y ) e. _V
7 f1oun 
 |-  ( ( ( x : A -1-1-onto-> B /\ y : C -1-1-onto-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( x u. y ) : ( A u. C ) -1-1-onto-> ( B u. D ) )
8 f1oen3g 
 |-  ( ( ( x u. y ) e. _V /\ ( x u. y ) : ( A u. C ) -1-1-onto-> ( B u. D ) ) -> ( A u. C ) ~~ ( B u. D ) )
9 6 7 8 sylancr 
 |-  ( ( ( x : A -1-1-onto-> B /\ y : C -1-1-onto-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( A u. C ) ~~ ( B u. D ) )
10 9 ex 
 |-  ( ( x : A -1-1-onto-> B /\ y : C -1-1-onto-> D ) -> ( ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) -> ( A u. C ) ~~ ( B u. D ) ) )
11 10 exlimivv 
 |-  ( E. x E. y ( x : A -1-1-onto-> B /\ y : C -1-1-onto-> D ) -> ( ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) -> ( A u. C ) ~~ ( B u. D ) ) )
12 3 11 sylbir 
 |-  ( ( E. x x : A -1-1-onto-> B /\ E. y y : C -1-1-onto-> D ) -> ( ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) -> ( A u. C ) ~~ ( B u. D ) ) )
13 1 2 12 syl2anb 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) -> ( A u. C ) ~~ ( B u. D ) ) )
14 13 imp 
 |-  ( ( ( A ~~ B /\ C ~~ D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( A u. C ) ~~ ( B u. D ) )