smfpimcclem

Description: Lemma for smfpimcc given the choice function C . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smfpimcclem.n	$⊢ Ⅎ n φ$
	smfpimcclem.z	$⊢ Z \in V$
	smfpimcclem.s	$⊢ φ \to S \in W$
	smfpimcclem.c	$⊢ (φ \land y \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})) \to C (y) \in y$
	smfpimcclem.h	$⊢ H = (n \in Z ⟼ C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}))$
Assertion	smfpimcclem	$⊢ φ \to \exists h (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n))$

Proof

Step	Hyp	Ref	Expression
1		smfpimcclem.n	$⊢ Ⅎ n φ$
2		smfpimcclem.z	$⊢ Z \in V$
3		smfpimcclem.s	$⊢ φ \to S \in W$
4		smfpimcclem.c	$⊢ (φ \land y \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})) \to C (y) \in y$
5		smfpimcclem.h	$⊢ H = (n \in Z ⟼ C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}))$
6		nfcv	$⊢ \underline{Ⅎ} s S$
7	6	ssrab2f	$⊢ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \subseteq S$
8		eqid	$⊢ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} = \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}$
9	8 3	rabexd	$⊢ φ \to \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in V$
10	9	adantr	$⊢ (φ \land n \in Z) \to \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in V$
11		simpl	$⊢ (φ \land n \in Z) \to φ$
12		simpr	$⊢ (φ \land n \in Z) \to n \in Z$
13		eqid	$⊢ (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) = (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})$
14	13	elrnmpt1	$⊢ (n \in Z \land \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in V) \to \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})$
15	12 10 14	syl2anc	$⊢ (φ \land n \in Z) \to \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})$
16	11 15	jca	$⊢ (φ \land n \in Z) \to (φ \land \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}))$
17		eleq1	$⊢ y = \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \to (y \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \leftrightarrow \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}))$
18	17	anbi2d	$⊢ y = \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \to ((φ \land y \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})) \leftrightarrow (φ \land \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})))$
19		fveq2	$⊢ y = \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \to C (y) = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})$
20		id	$⊢ y = \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \to y = \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}$
21	19 20	eleq12d	$⊢ y = \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \to (C (y) \in y \leftrightarrow C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})$
22	18 21	imbi12d	$⊢ y = \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \to (((φ \land y \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})) \to C (y) \in y) \leftrightarrow ((φ \land \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})) \to C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}))$
23	22 4	vtoclg	$⊢ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in V \to ((φ \land \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in ran (n \in Z ⟼ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})) \to C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})$
24	10 16 23	sylc	$⊢ (φ \land n \in Z) \to C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}$
25	7 24	sselid	$⊢ (φ \land n \in Z) \to C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in S$
26	1 25 5	fmptdf	$⊢ φ \to H : Z ⟶ S$
27		nfcv	$⊢ \underline{Ⅎ} s C$
28		nfrab1	$⊢ \underline{Ⅎ} s \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}$
29	27 28	nffv	$⊢ \underline{Ⅎ} s C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})$
30		nfcv	$⊢ \underline{Ⅎ} s {F (n)}^{-1} [A]$
31		nfcv	$⊢ \underline{Ⅎ} s dom F (n)$
32	29 31	nfin	$⊢ \underline{Ⅎ} s (C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \cap dom F (n))$
33	30 32	nfeq	$⊢ Ⅎ s {F (n)}^{-1} [A] = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \cap dom F (n)$
34		ineq1	$⊢ s = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \to s \cap dom F (n) = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \cap dom F (n)$
35	34	eqeq2d	$⊢ s = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \to ({F (n)}^{-1} [A] = s \cap dom F (n) \leftrightarrow {F (n)}^{-1} [A] = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \cap dom F (n))$
36	29 6 33 35	elrabf	$⊢ C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \leftrightarrow (C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in S \land {F (n)}^{-1} [A] = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \cap dom F (n))$
37	24 36	sylib	$⊢ (φ \land n \in Z) \to (C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in S \land {F (n)}^{-1} [A] = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \cap dom F (n))$
38	37	simprd	$⊢ (φ \land n \in Z) \to {F (n)}^{-1} [A] = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \cap dom F (n)$
39	5	a1i	$⊢ φ \to H = (n \in Z ⟼ C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}))$
40	24	elexd	$⊢ (φ \land n \in Z) \to C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in V$
41	39 40	fvmpt2d	$⊢ (φ \land n \in Z) \to H (n) = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})$
42	41	ineq1d	$⊢ (φ \land n \in Z) \to H (n) \cap dom F (n) = C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \cap dom F (n)$
43	38 42	eqtr4d	$⊢ (φ \land n \in Z) \to {F (n)}^{-1} [A] = H (n) \cap dom F (n)$
44	43	ex	$⊢ φ \to (n \in Z \to {F (n)}^{-1} [A] = H (n) \cap dom F (n))$
45	1 44	ralrimi	$⊢ φ \to \forall n \in Z {F (n)}^{-1} [A] = H (n) \cap dom F (n)$
46	2	elexi	$⊢ Z \in V$
47	46	mptex	$⊢ (n \in Z ⟼ C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})) \in V$
48	5 47	eqeltri	$⊢ H \in V$
49		feq1	$⊢ h = H \to (h : Z ⟶ S \leftrightarrow H : Z ⟶ S)$
50		nfcv	$⊢ \underline{Ⅎ} n h$
51		nfmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}))$
52	5 51	nfcxfr	$⊢ \underline{Ⅎ} n H$
53	50 52	nfeq	$⊢ Ⅎ n h = H$
54		fveq1	$⊢ h = H \to h (n) = H (n)$
55	54	ineq1d	$⊢ h = H \to h (n) \cap dom F (n) = H (n) \cap dom F (n)$
56	55	eqeq2d	$⊢ h = H \to ({F (n)}^{-1} [A] = h (n) \cap dom F (n) \leftrightarrow {F (n)}^{-1} [A] = H (n) \cap dom F (n))$
57	53 56	ralbid	$⊢ h = H \to (\forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n) \leftrightarrow \forall n \in Z {F (n)}^{-1} [A] = H (n) \cap dom F (n))$
58	49 57	anbi12d	$⊢ h = H \to ((h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n)) \leftrightarrow (H : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = H (n) \cap dom F (n)))$
59	48 58	spcev	$⊢ (H : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = H (n) \cap dom F (n)) \to \exists h (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n))$
60	26 45 59	syl2anc	$⊢ φ \to \exists h (h : Z ⟶ S \land \forall n \in Z {F (n)}^{-1} [A] = h (n) \cap dom F (n))$

Metamath Proof Explorer

Theorem smfpimcclem

Proof