This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
marypha1.b ⊢ ( 𝜑 → 𝐵 ∈ Fin )
marypha1.c ⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐴 × 𝐵 ) )
marypha1.d ⊢ ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → 𝑑 ≼ ( 𝐶 “ 𝑑 ) )
Assertion marypha1 ( 𝜑 → ∃ 𝑓 ∈ 𝒫 𝐶 𝑓 : 𝐴 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 marypha1.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 marypha1.b ⊢ ( 𝜑 → 𝐵 ∈ Fin )
3 marypha1.c ⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐴 × 𝐵 ) )
4 marypha1.d ⊢ ( ( 𝜑 ∧ 𝑑 ⊆ 𝐴 ) → 𝑑 ≼ ( 𝐶 “ 𝑑 ) )
5 elpwi ⊢ ( 𝑑 ∈ 𝒫 𝐴 → 𝑑 ⊆ 𝐴 )
6 5 4 sylan2 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝒫 𝐴 ) → 𝑑 ≼ ( 𝐶 “ 𝑑 ) )
7 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝐶 “ 𝑑 ) )
8 imaeq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 “ 𝑑 ) = ( 𝐶 “ 𝑑 ) )
9 8 breq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑑 ≼ ( 𝑐 “ 𝑑 ) ↔ 𝑑 ≼ ( 𝐶 “ 𝑑 ) ) )
10 9 ralbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) ↔ ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝐶 “ 𝑑 ) ) )
11 pweq ⊢ ( 𝑐 = 𝐶 → 𝒫 𝑐 = 𝒫 𝐶 )
12 11 rexeqdv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ↔ ∃ 𝑓 ∈ 𝒫 𝐶 𝑓 : 𝐴 –1-1→ V ) )
13 10 12 imbi12d ⊢ ( 𝑐 = 𝐶 → ( ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ) ↔ ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝐶 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝐶 𝑓 : 𝐴 –1-1→ V ) ) )
14 xpeq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 × 𝑏 ) = ( 𝐴 × 𝐵 ) )
15 14 pweqd ⊢ ( 𝑏 = 𝐵 → 𝒫 ( 𝐴 × 𝑏 ) = 𝒫 ( 𝐴 × 𝐵 ) )
16 15 raleqdv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ) ↔ ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝐵 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ) ) )
17 16 imbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ) ) ↔ ( 𝐴 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝐵 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ) ) ) )
18 marypha1lem ⊢ ( 𝐴 ∈ Fin → ( 𝑏 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ) ) )
19 18 com12 ⊢ ( 𝑏 ∈ Fin → ( 𝐴 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝑏 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ) ) )
20 17 19 vtoclga ⊢ ( 𝐵 ∈ Fin → ( 𝐴 ∈ Fin → ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝐵 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ) ) )
21 2 1 20 sylc ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝒫 ( 𝐴 × 𝐵 ) ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝑐 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝑐 𝑓 : 𝐴 –1-1→ V ) )
22 1 2 xpexd ⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
23 22 3 sselpwd ⊢ ( 𝜑 → 𝐶 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
24 13 21 23 rspcdva ⊢ ( 𝜑 → ( ∀ 𝑑 ∈ 𝒫 𝐴 𝑑 ≼ ( 𝐶 “ 𝑑 ) → ∃ 𝑓 ∈ 𝒫 𝐶 𝑓 : 𝐴 –1-1→ V ) )
25 7 24 mpd ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝒫 𝐶 𝑓 : 𝐴 –1-1→ V )
26 elpwi ⊢ ( 𝑓 ∈ 𝒫 𝐶 → 𝑓 ⊆ 𝐶 )
27 26 3 sylan9ssr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝒫 𝐶 ) → 𝑓 ⊆ ( 𝐴 × 𝐵 ) )
28 rnss ⊢ ( 𝑓 ⊆ ( 𝐴 × 𝐵 ) → ran 𝑓 ⊆ ran ( 𝐴 × 𝐵 ) )
29 27 28 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝒫 𝐶 ) → ran 𝑓 ⊆ ran ( 𝐴 × 𝐵 ) )
30 rnxpss ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
31 29 30 sstrdi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝒫 𝐶 ) → ran 𝑓 ⊆ 𝐵 )
32 f1ssr ⊢ ( ( 𝑓 : 𝐴 –1-1→ V ∧ ran 𝑓 ⊆ 𝐵 ) → 𝑓 : 𝐴 –1-1→ 𝐵 )
33 32 expcom ⊢ ( ran 𝑓 ⊆ 𝐵 → ( 𝑓 : 𝐴 –1-1→ V → 𝑓 : 𝐴 –1-1→ 𝐵 ) )
34 31 33 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝒫 𝐶 ) → ( 𝑓 : 𝐴 –1-1→ V → 𝑓 : 𝐴 –1-1→ 𝐵 ) )
35 34 reximdva ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ 𝒫 𝐶 𝑓 : 𝐴 –1-1→ V → ∃ 𝑓 ∈ 𝒫 𝐶 𝑓 : 𝐴 –1-1→ 𝐵 ) )
36 25 35 mpd ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝒫 𝐶 𝑓 : 𝐴 –1-1→ 𝐵 )