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		ssrab2	$⊢ \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \subseteq S$
7		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)\}$
8	7 3	rabexd	$⊢ φ \to \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in V$
9	8	adantr	$⊢ (φ \land n \in Z) \to \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\} \in V$
10		simpl	$⊢ (φ \land n \in Z) \to φ$
11		simpr	$⊢ (φ \land n \in Z) \to n \in Z$
12		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)\})$
13	12	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)\})$
14	11 9 13	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)\})$
15	10 14	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)\}))$
16		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)\}))$
17	16	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)\})))$
18		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)\})$
19		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)\}$
20	18 19	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)\})$
21	17 20	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)\}))$
22	21 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)\})$
23	9 15 22	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)\}$
24	6 23	sselid	$⊢ (φ \land n \in Z) \to C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}) \in S$
25	1 24 5	fmptdf	$⊢ φ \to H : Z ⟶ S$
26		nfcv	$⊢ \underline{Ⅎ} s C$
27		nfrab1	$⊢ \underline{Ⅎ} s \{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\}$
28	26 27	nffv	$⊢ \underline{Ⅎ} s C (\{s \in S \| {F (n)}^{-1} [A] = s \cap dom F (n)\})$
29		nfcv	$⊢ \underline{Ⅎ} s S$
30		nfcv	$⊢ \underline{Ⅎ} s {F (n)}^{-1} [A]$
31		nfcv	$⊢ \underline{Ⅎ} s dom F (n)$
32	28 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	28 29 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	23 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	23	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	25 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