marypha2

Description: Version of marypha1 using a functional family of sets instead of a relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

	Ref	Expression
Hypotheses	marypha2.a	$⊢ φ \to A \in Fin$
	marypha2.b	$⊢ φ \to F : A ⟶ Fin$
	marypha2.c	$⊢ (φ \land d \subseteq A) \to d ≼ ⋃ F [d]$
Assertion	marypha2	$⊢ φ \to \exists g (g : A \underset{1-1}{⟶} V \land \forall x \in A g (x) \in F (x))$

Proof

Step	Hyp	Ref	Expression
1		marypha2.a	$⊢ φ \to A \in Fin$
2		marypha2.b	$⊢ φ \to F : A ⟶ Fin$
3		marypha2.c	$⊢ (φ \land d \subseteq A) \to d ≼ ⋃ F [d]$
4	2 1	unirnffid	$⊢ φ \to ⋃ ran F \in Fin$
5		eqid	$⊢ ⋃_{x \in A} (\{x\} \times F (x)) = ⋃_{x \in A} (\{x\} \times F (x))$
6	5	marypha2lem1	$⊢ ⋃_{x \in A} (\{x\} \times F (x)) \subseteq A \times ⋃ ran F$
7	6	a1i	$⊢ φ \to ⋃_{x \in A} (\{x\} \times F (x)) \subseteq A \times ⋃ ran F$
8	2	ffnd	$⊢ φ \to F Fn A$
9	5	marypha2lem4	$⊢ (F Fn A \land d \subseteq A) \to ⋃_{x \in A} (\{x\} \times F (x)) [d] = ⋃ F [d]$
10	8 9	sylan	$⊢ (φ \land d \subseteq A) \to ⋃_{x \in A} (\{x\} \times F (x)) [d] = ⋃ F [d]$
11	3 10	breqtrrd	$⊢ (φ \land d \subseteq A) \to d ≼ ⋃_{x \in A} (\{x\} \times F (x)) [d]$
12	1 4 7 11	marypha1	$⊢ φ \to \exists g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) g : A \underset{1-1}{⟶} ⋃ ran F$
13		df-rex	$⊢ \exists g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) g : A \underset{1-1}{⟶} ⋃ ran F \leftrightarrow \exists g (g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \land g : A \underset{1-1}{⟶} ⋃ ran F)$
14		ssv	$⊢ ⋃ ran F \subseteq V$
15		f1ss	$⊢ (g : A \underset{1-1}{⟶} ⋃ ran F \land ⋃ ran F \subseteq V) \to g : A \underset{1-1}{⟶} V$
16	14 15	mpan2	$⊢ g : A \underset{1-1}{⟶} ⋃ ran F \to g : A \underset{1-1}{⟶} V$
17	16	ad2antll	$⊢ (φ \land (g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \land g : A \underset{1-1}{⟶} ⋃ ran F)) \to g : A \underset{1-1}{⟶} V$
18		elpwi	$⊢ g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \to g \subseteq ⋃_{x \in A} (\{x\} \times F (x))$
19	18	ad2antrl	$⊢ (φ \land (g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \land g : A \underset{1-1}{⟶} ⋃ ran F)) \to g \subseteq ⋃_{x \in A} (\{x\} \times F (x))$
20		f1fn	$⊢ g : A \underset{1-1}{⟶} ⋃ ran F \to g Fn A$
21	20	ad2antll	$⊢ (φ \land (g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \land g : A \underset{1-1}{⟶} ⋃ ran F)) \to g Fn A$
22	5	marypha2lem3	$⊢ (F Fn A \land g Fn A) \to (g \subseteq ⋃_{x \in A} (\{x\} \times F (x)) \leftrightarrow \forall x \in A g (x) \in F (x))$
23	8 21 22	syl2an2r	$⊢ (φ \land (g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \land g : A \underset{1-1}{⟶} ⋃ ran F)) \to (g \subseteq ⋃_{x \in A} (\{x\} \times F (x)) \leftrightarrow \forall x \in A g (x) \in F (x))$
24	19 23	mpbid	$⊢ (φ \land (g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \land g : A \underset{1-1}{⟶} ⋃ ran F)) \to \forall x \in A g (x) \in F (x)$
25	17 24	jca	$⊢ (φ \land (g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \land g : A \underset{1-1}{⟶} ⋃ ran F)) \to (g : A \underset{1-1}{⟶} V \land \forall x \in A g (x) \in F (x))$
26	25	ex	$⊢ φ \to ((g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \land g : A \underset{1-1}{⟶} ⋃ ran F) \to (g : A \underset{1-1}{⟶} V \land \forall x \in A g (x) \in F (x)))$
27	26	eximdv	$⊢ φ \to (\exists g (g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) \land g : A \underset{1-1}{⟶} ⋃ ran F) \to \exists g (g : A \underset{1-1}{⟶} V \land \forall x \in A g (x) \in F (x)))$
28	13 27	syl5bi	$⊢ φ \to (\exists g \in 𝒫 ⋃_{x \in A} (\{x\} \times F (x)) g : A \underset{1-1}{⟶} ⋃ ran F \to \exists g (g : A \underset{1-1}{⟶} V \land \forall x \in A g (x) \in F (x)))$
29	12 28	mpd	$⊢ φ \to \exists g (g : A \underset{1-1}{⟶} V \land \forall x \in A g (x) \in F (x))$

Metamath Proof Explorer

Theorem marypha2

Proof