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→ 𝐵 )