# 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 $⊢ φ → A ∈ Fin$
marypha1.b $⊢ φ → B ∈ Fin$
marypha1.c $⊢ φ → C ⊆ A × B$
marypha1.d $⊢ φ ∧ d ⊆ A → d ≼ C d$
Assertion marypha1 $⊢ φ → ∃ f ∈ 𝒫 C f : A ⟶ 1-1 B$

### Proof

Step Hyp Ref Expression
1 marypha1.a $⊢ φ → A ∈ Fin$
2 marypha1.b $⊢ φ → B ∈ Fin$
3 marypha1.c $⊢ φ → C ⊆ A × B$
4 marypha1.d $⊢ φ ∧ d ⊆ A → d ≼ C d$
5 elpwi $⊢ d ∈ 𝒫 A → d ⊆ A$
6 5 4 sylan2 $⊢ φ ∧ d ∈ 𝒫 A → d ≼ C d$
7 6 ralrimiva $⊢ φ → ∀ d ∈ 𝒫 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 → ∀ d ∈ 𝒫 A d ≼ c d ↔ ∀ d ∈ 𝒫 A d ≼ C d$
11 pweq $⊢ c = C → 𝒫 c = 𝒫 C$
12 11 rexeqdv $⊢ c = C → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V ↔ ∃ f ∈ 𝒫 C f : A ⟶ 1-1 V$
13 10 12 imbi12d $⊢ c = C → ∀ d ∈ 𝒫 A d ≼ c d → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V ↔ ∀ d ∈ 𝒫 A d ≼ C d → ∃ f ∈ 𝒫 C f : A ⟶ 1-1 V$
14 xpeq2 $⊢ b = B → A × b = A × B$
15 14 pweqd $⊢ b = B → 𝒫 A × b = 𝒫 A × B$
16 15 raleqdv $⊢ b = B → ∀ c ∈ 𝒫 A × b ∀ d ∈ 𝒫 A d ≼ c d → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V ↔ ∀ c ∈ 𝒫 A × B ∀ d ∈ 𝒫 A d ≼ c d → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V$
17 16 imbi2d $⊢ b = B → A ∈ Fin → ∀ c ∈ 𝒫 A × b ∀ d ∈ 𝒫 A d ≼ c d → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V ↔ A ∈ Fin → ∀ c ∈ 𝒫 A × B ∀ d ∈ 𝒫 A d ≼ c d → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V$
18 marypha1lem $⊢ A ∈ Fin → b ∈ Fin → ∀ c ∈ 𝒫 A × b ∀ d ∈ 𝒫 A d ≼ c d → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V$
19 18 com12 $⊢ b ∈ Fin → A ∈ Fin → ∀ c ∈ 𝒫 A × b ∀ d ∈ 𝒫 A d ≼ c d → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V$
20 17 19 vtoclga $⊢ B ∈ Fin → A ∈ Fin → ∀ c ∈ 𝒫 A × B ∀ d ∈ 𝒫 A d ≼ c d → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V$
21 2 1 20 sylc $⊢ φ → ∀ c ∈ 𝒫 A × B ∀ d ∈ 𝒫 A d ≼ c d → ∃ f ∈ 𝒫 c f : A ⟶ 1-1 V$
22 1 2 xpexd $⊢ φ → A × B ∈ V$
23 22 3 sselpwd $⊢ φ → C ∈ 𝒫 A × B$
24 13 21 23 rspcdva $⊢ φ → ∀ d ∈ 𝒫 A d ≼ C d → ∃ f ∈ 𝒫 C f : A ⟶ 1-1 V$
25 7 24 mpd $⊢ φ → ∃ f ∈ 𝒫 C f : A ⟶ 1-1 V$
26 elpwi $⊢ f ∈ 𝒫 C → f ⊆ C$
27 26 3 sylan9ssr $⊢ φ ∧ f ∈ 𝒫 C → f ⊆ A × B$
28 rnss $⊢ f ⊆ A × B → ran ⁡ f ⊆ ran ⁡ A × B$
29 27 28 syl $⊢ φ ∧ f ∈ 𝒫 C → ran ⁡ f ⊆ ran ⁡ A × B$
30 rnxpss $⊢ ran ⁡ A × B ⊆ B$
31 29 30 sstrdi $⊢ φ ∧ f ∈ 𝒫 C → ran ⁡ f ⊆ B$
32 f1ssr $⊢ f : A ⟶ 1-1 V ∧ ran ⁡ f ⊆ B → f : A ⟶ 1-1 B$
33 32 expcom $⊢ ran ⁡ f ⊆ B → f : A ⟶ 1-1 V → f : A ⟶ 1-1 B$
34 31 33 syl $⊢ φ ∧ f ∈ 𝒫 C → f : A ⟶ 1-1 V → f : A ⟶ 1-1 B$
35 34 reximdva $⊢ φ → ∃ f ∈ 𝒫 C f : A ⟶ 1-1 V → ∃ f ∈ 𝒫 C f : A ⟶ 1-1 B$
36 25 35 mpd $⊢ φ → ∃ f ∈ 𝒫 C f : A ⟶ 1-1 B$