Metamath Proof Explorer

Theorem marypha1

Description: (Philip) Hall's marriage theorem, sufficiency: a finite relation contains an injection if there is no subset of its domain which would be forced to violate the pigeonhole principle. (Contributed by Stefan O'Rear, 20-Feb-2015)

Ref Expression
Hypotheses marypha1.a 
|- ( ph -> A e. Fin )
marypha1.b 
|- ( ph -> B e. Fin )
marypha1.c 
|- ( ph -> C C_ ( A X. B ) )
marypha1.d 
|- ( ( ph /\ d C_ A ) -> d ~<_ ( C " d ) )
Assertion marypha1 
|- ( ph -> E. f e. ~P C f : A -1-1-> B )

Proof

Step Hyp Ref Expression
1 marypha1.a 
 |-  ( ph -> A e. Fin )
2 marypha1.b 
 |-  ( ph -> B e. Fin )
3 marypha1.c 
 |-  ( ph -> C C_ ( A X. B ) )
4 marypha1.d 
 |-  ( ( ph /\ d C_ A ) -> d ~<_ ( C " d ) )
5 elpwi 
 |-  ( d e. ~P A -> d C_ A )
6 5 4 sylan2 
 |-  ( ( ph /\ d e. ~P A ) -> d ~<_ ( C " d ) )
7 6 ralrimiva 
 |-  ( ph -> A. d e. ~P A d ~<_ ( C " d ) )
8 imaeq1 
 |-  ( c = C -> ( c " d ) = ( C " d ) )
9 8 breq2d 
 |-  ( c = C -> ( d ~<_ ( c " d ) <-> d ~<_ ( C " d ) ) )
10 9 ralbidv 
 |-  ( c = C -> ( A. d e. ~P A d ~<_ ( c " d ) <-> A. d e. ~P A d ~<_ ( C " d ) ) )
11 pweq 
 |-  ( c = C -> ~P c = ~P C )
12 11 rexeqdv 
 |-  ( c = C -> ( E. f e. ~P c f : A -1-1-> _V <-> E. f e. ~P C f : A -1-1-> _V ) )
13 10 12 imbi12d 
 |-  ( c = C -> ( ( A. d e. ~P A d ~<_ ( c " d ) -> E. f e. ~P c f : A -1-1-> _V ) <-> ( A. d e. ~P A d ~<_ ( C " d ) -> E. f e. ~P C f : A -1-1-> _V ) ) )
14 xpeq2 
 |-  ( b = B -> ( A X. b ) = ( A X. B ) )
15 14 pweqd 
 |-  ( b = B -> ~P ( A X. b ) = ~P ( A X. B ) )
16 15 raleqdv 
 |-  ( b = B -> ( A. c e. ~P ( A X. b ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. f e. ~P c f : A -1-1-> _V ) <-> A. c e. ~P ( A X. B ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. f e. ~P c f : A -1-1-> _V ) ) )
17 16 imbi2d 
 |-  ( b = B -> ( ( A e. Fin -> A. c e. ~P ( A X. b ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. f e. ~P c f : A -1-1-> _V ) ) <-> ( A e. Fin -> A. c e. ~P ( A X. B ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. f e. ~P c f : A -1-1-> _V ) ) ) )
18 marypha1lem 
 |-  ( A e. Fin -> ( b e. Fin -> A. c e. ~P ( A X. b ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. f e. ~P c f : A -1-1-> _V ) ) )
19 18 com12 
 |-  ( b e. Fin -> ( A e. Fin -> A. c e. ~P ( A X. b ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. f e. ~P c f : A -1-1-> _V ) ) )
20 17 19 vtoclga 
 |-  ( B e. Fin -> ( A e. Fin -> A. c e. ~P ( A X. B ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. f e. ~P c f : A -1-1-> _V ) ) )
21 2 1 20 sylc 
 |-  ( ph -> A. c e. ~P ( A X. B ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. f e. ~P c f : A -1-1-> _V ) )
22 1 2 xpexd 
 |-  ( ph -> ( A X. B ) e. _V )
23 22 3 sselpwd 
 |-  ( ph -> C e. ~P ( A X. B ) )
24 13 21 23 rspcdva 
 |-  ( ph -> ( A. d e. ~P A d ~<_ ( C " d ) -> E. f e. ~P C f : A -1-1-> _V ) )
25 7 24 mpd 
 |-  ( ph -> E. f e. ~P C f : A -1-1-> _V )
26 elpwi 
 |-  ( f e. ~P C -> f C_ C )
27 26 3 sylan9ssr 
 |-  ( ( ph /\ f e. ~P C ) -> f C_ ( A X. B ) )
28 rnss 
 |-  ( f C_ ( A X. B ) -> ran f C_ ran ( A X. B ) )
29 27 28 syl 
 |-  ( ( ph /\ f e. ~P C ) -> ran f C_ ran ( A X. B ) )
30 rnxpss 
 |-  ran ( A X. B ) C_ B
31 29 30 sstrdi 
 |-  ( ( ph /\ f e. ~P C ) -> ran f C_ B )
32 f1ssr 
 |-  ( ( f : A -1-1-> _V /\ ran f C_ B ) -> f : A -1-1-> B )
33 32 expcom 
 |-  ( ran f C_ B -> ( f : A -1-1-> _V -> f : A -1-1-> B ) )
34 31 33 syl 
 |-  ( ( ph /\ f e. ~P C ) -> ( f : A -1-1-> _V -> f : A -1-1-> B ) )
35 34 reximdva 
 |-  ( ph -> ( E. f e. ~P C f : A -1-1-> _V -> E. f e. ~P C f : A -1-1-> B ) )
36 25 35 mpd 
 |-  ( ph -> E. f e. ~P C f : A -1-1-> B )