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	$⊢ φ \to A \in Fin$
	marypha1.b	$⊢ φ \to B \in Fin$
	marypha1.c	$⊢ φ \to C \subseteq A \times B$
	marypha1.d	$⊢ (φ \land d \subseteq A) \to d ≼ C [d]$
Assertion	marypha1	$⊢ φ \to \exists f \in 𝒫 C f : A \underset{1-1}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		marypha1.a	$⊢ φ \to A \in Fin$
2		marypha1.b	$⊢ φ \to B \in Fin$
3		marypha1.c	$⊢ φ \to C \subseteq A \times B$
4		marypha1.d	$⊢ (φ \land d \subseteq A) \to d ≼ C [d]$
5		elpwi	$⊢ d \in 𝒫 A \to d \subseteq A$
6	5 4	sylan2	$⊢ (φ \land d \in 𝒫 A) \to d ≼ C [d]$
7	6	ralrimiva	$⊢ φ \to \forall d \in 𝒫 A d ≼ C [d]$
8		imaeq1	$⊢ c = C \to c [d] = C [d]$
9	8	breq2d	$⊢ c = C \to (d ≼ c [d] \leftrightarrow d ≼ C [d])$
10	9	ralbidv	$⊢ c = C \to (\forall d \in 𝒫 A d ≼ c [d] \leftrightarrow \forall d \in 𝒫 A d ≼ C [d])$
11		pweq	$⊢ c = C \to 𝒫 c = 𝒫 C$
12	11	rexeqdv	$⊢ c = C \to (\exists f \in 𝒫 c f : A \underset{1-1}{⟶} V \leftrightarrow \exists f \in 𝒫 C f : A \underset{1-1}{⟶} V)$
13	10 12	imbi12d	$⊢ c = C \to ((\forall d \in 𝒫 A d ≼ c [d] \to \exists f \in 𝒫 c f : A \underset{1-1}{⟶} V) \leftrightarrow (\forall d \in 𝒫 A d ≼ C [d] \to \exists f \in 𝒫 C f : A \underset{1-1}{⟶} V))$
14		xpeq2	$⊢ b = B \to A \times b = A \times B$
15	14	pweqd	$⊢ b = B \to 𝒫 (A \times b) = 𝒫 (A \times B)$
16	15	raleqdv	$⊢ b = B \to (\forall c \in 𝒫 (A \times b) (\forall d \in 𝒫 A d ≼ c [d] \to \exists f \in 𝒫 c f : A \underset{1-1}{⟶} V) \leftrightarrow \forall c \in 𝒫 (A \times B) (\forall d \in 𝒫 A d ≼ c [d] \to \exists f \in 𝒫 c f : A \underset{1-1}{⟶} V))$
17	16	imbi2d	$⊢ b = B \to ((A \in Fin \to \forall c \in 𝒫 (A \times b) (\forall d \in 𝒫 A d ≼ c [d] \to \exists f \in 𝒫 c f : A \underset{1-1}{⟶} V)) \leftrightarrow (A \in Fin \to \forall c \in 𝒫 (A \times B) (\forall d \in 𝒫 A d ≼ c [d] \to \exists f \in 𝒫 c f : A \underset{1-1}{⟶} V)))$
18		marypha1lem	$⊢ A \in Fin \to (b \in Fin \to \forall c \in 𝒫 (A \times b) (\forall d \in 𝒫 A d ≼ c [d] \to \exists f \in 𝒫 c f : A \underset{1-1}{⟶} V))$
19	18	com12	$⊢ b \in Fin \to (A \in Fin \to \forall c \in 𝒫 (A \times b) (\forall d \in 𝒫 A d ≼ c [d] \to \exists f \in 𝒫 c f : A \underset{1-1}{⟶} V))$
20	17 19	vtoclga	$⊢ B \in Fin \to (A \in Fin \to \forall c \in 𝒫 (A \times B) (\forall d \in 𝒫 A d ≼ c [d] \to \exists f \in 𝒫 c f : A \underset{1-1}{⟶} V))$
21	2 1 20	sylc	$⊢ φ \to \forall c \in 𝒫 (A \times B) (\forall d \in 𝒫 A d ≼ c [d] \to \exists f \in 𝒫 c f : A \underset{1-1}{⟶} V)$
22	1 2	xpexd	$⊢ φ \to A \times B \in V$
23	22 3	sselpwd	$⊢ φ \to C \in 𝒫 (A \times B)$
24	13 21 23	rspcdva	$⊢ φ \to (\forall d \in 𝒫 A d ≼ C [d] \to \exists f \in 𝒫 C f : A \underset{1-1}{⟶} V)$
25	7 24	mpd	$⊢ φ \to \exists f \in 𝒫 C f : A \underset{1-1}{⟶} V$
26		elpwi	$⊢ f \in 𝒫 C \to f \subseteq C$
27	26 3	sylan9ssr	$⊢ (φ \land f \in 𝒫 C) \to f \subseteq A \times B$
28		rnss	$⊢ f \subseteq A \times B \to ran f \subseteq ran (A \times B)$
29	27 28	syl	$⊢ (φ \land f \in 𝒫 C) \to ran f \subseteq ran (A \times B)$
30		rnxpss	$⊢ ran (A \times B) \subseteq B$
31	29 30	sstrdi	$⊢ (φ \land f \in 𝒫 C) \to ran f \subseteq B$
32		f1ssr	$⊢ (f : A \underset{1-1}{⟶} V \land ran f \subseteq B) \to f : A \underset{1-1}{⟶} B$
33	32	expcom	$⊢ ran f \subseteq B \to (f : A \underset{1-1}{⟶} V \to f : A \underset{1-1}{⟶} B)$
34	31 33	syl	$⊢ (φ \land f \in 𝒫 C) \to (f : A \underset{1-1}{⟶} V \to f : A \underset{1-1}{⟶} B)$
35	34	reximdva	$⊢ φ \to (\exists f \in 𝒫 C f : A \underset{1-1}{⟶} V \to \exists f \in 𝒫 C f : A \underset{1-1}{⟶} B)$
36	25 35	mpd	$⊢ φ \to \exists f \in 𝒫 C f : A \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem marypha1

Proof