fnrelpredd

Description: A function that preserves a relation also preserves predecessors. (Contributed by BTernaryTau, 16-Jul-2024)

	Ref	Expression
Hypotheses	fnrelpredd.1	$⊢ φ \to F Fn A$
	fnrelpredd.2	$⊢ φ \to \forall x \in A \forall y \in A (x R y \leftrightarrow F (x) S F (y))$
	fnrelpredd.3	$⊢ φ \to C \subseteq A$
	fnrelpredd.4	$⊢ φ \to D \in A$
Assertion	fnrelpredd	$⊢ φ \to Pred (S, F [C], F (D)) = F [Pred (R, C, D)]$

Proof

Step	Hyp	Ref	Expression
1		fnrelpredd.1	$⊢ φ \to F Fn A$
2		fnrelpredd.2	$⊢ φ \to \forall x \in A \forall y \in A (x R y \leftrightarrow F (x) S F (y))$
3		fnrelpredd.3	$⊢ φ \to C \subseteq A$
4		fnrelpredd.4	$⊢ φ \to D \in A$
5		fvex	$⊢ F (D) \in V$
6	5	dfpred3	$⊢ Pred (S, F [C], F (D)) = \{v \in F [C] \| v S F (D)\}$
7		elrabi	$⊢ u \in \{x \in C \| F (x) S F (D)\} \to u \in C$
8	7	anim1i	$⊢ (u \in \{x \in C \| F (x) S F (D)\} \land F (u) = v) \to (u \in C \land F (u) = v)$
9	8	reximi2	$⊢ \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v \to \exists u \in C F (u) = v$
10	1 3	fvelimabd	$⊢ φ \to (v \in F [C] \leftrightarrow \exists u \in C F (u) = v)$
11	9 10	imbitrrid	$⊢ φ \to (\exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v \to v \in F [C])$
12		fveq2	$⊢ x = u \to F (x) = F (u)$
13	12	breq1d	$⊢ x = u \to (F (x) S F (D) \leftrightarrow F (u) S F (D))$
14	13	elrab	$⊢ u \in \{x \in C \| F (x) S F (D)\} \leftrightarrow (u \in C \land F (u) S F (D))$
15		breq1	$⊢ F (u) = v \to (F (u) S F (D) \leftrightarrow v S F (D))$
16	15	biimpac	$⊢ (F (u) S F (D) \land F (u) = v) \to v S F (D)$
17	16	adantll	$⊢ ((u \in C \land F (u) S F (D)) \land F (u) = v) \to v S F (D)$
18	14 17	sylanb	$⊢ (u \in \{x \in C \| F (x) S F (D)\} \land F (u) = v) \to v S F (D)$
19	18	rexlimiva	$⊢ \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v \to v S F (D)$
20	11 19	jca2	$⊢ φ \to (\exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v \to (v \in F [C] \land v S F (D)))$
21	10	biimpd	$⊢ φ \to (v \in F [C] \to \exists u \in C F (u) = v)$
22	21	adantrd	$⊢ φ \to ((v \in F [C] \land v S F (D)) \to \exists u \in C F (u) = v)$
23		simpl	$⊢ (u \in C \land F (u) = v) \to u \in C$
24	23	a1i	$⊢ v S F (D) \to ((u \in C \land F (u) = v) \to u \in C)$
25	15	biimprcd	$⊢ v S F (D) \to (F (u) = v \to F (u) S F (D))$
26	25	adantld	$⊢ v S F (D) \to ((u \in C \land F (u) = v) \to F (u) S F (D))$
27		simpr	$⊢ (u \in C \land F (u) = v) \to F (u) = v$
28	27	a1i	$⊢ v S F (D) \to ((u \in C \land F (u) = v) \to F (u) = v)$
29	24 26 28	3jcad	$⊢ v S F (D) \to ((u \in C \land F (u) = v) \to (u \in C \land F (u) S F (D) \land F (u) = v))$
30	14	biimpri	$⊢ (u \in C \land F (u) S F (D)) \to u \in \{x \in C \| F (x) S F (D)\}$
31	30	anim1i	$⊢ ((u \in C \land F (u) S F (D)) \land F (u) = v) \to (u \in \{x \in C \| F (x) S F (D)\} \land F (u) = v)$
32	31	3impa	$⊢ (u \in C \land F (u) S F (D) \land F (u) = v) \to (u \in \{x \in C \| F (x) S F (D)\} \land F (u) = v)$
33	29 32	syl6	$⊢ v S F (D) \to ((u \in C \land F (u) = v) \to (u \in \{x \in C \| F (x) S F (D)\} \land F (u) = v))$
34	33	reximdv2	$⊢ v S F (D) \to (\exists u \in C F (u) = v \to \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v)$
35	34	adantl	$⊢ (v \in F [C] \land v S F (D)) \to (\exists u \in C F (u) = v \to \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v)$
36	22 35	sylcom	$⊢ φ \to ((v \in F [C] \land v S F (D)) \to \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v)$
37	20 36	impbid	$⊢ φ \to (\exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v \leftrightarrow (v \in F [C] \land v S F (D)))$
38	37	abbidv	$⊢ φ \to \{v \| \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v\} = \{v \| (v \in F [C] \land v S F (D))\}$
39		df-rab	$⊢ \{v \in F [C] \| v S F (D)\} = \{v \| (v \in F [C] \land v S F (D))\}$
40	38 39	eqtr4di	$⊢ φ \to \{v \| \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v\} = \{v \in F [C] \| v S F (D)\}$
41	6 40	eqtr4id	$⊢ φ \to Pred (S, F [C], F (D)) = \{v \| \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v\}$
42		fnfun	$⊢ F Fn A \to Fun F$
43	1 42	syl	$⊢ φ \to Fun F$
44		ssrab2	$⊢ \{x \in C \| F (x) S F (D)\} \subseteq C$
45	44 3	sstrid	$⊢ φ \to \{x \in C \| F (x) S F (D)\} \subseteq A$
46	1	fndmd	$⊢ φ \to dom F = A$
47	45 46	sseqtrrd	$⊢ φ \to \{x \in C \| F (x) S F (D)\} \subseteq dom F$
48		dfimafn	$⊢ (Fun F \land \{x \in C \| F (x) S F (D)\} \subseteq dom F) \to F [\{x \in C \| F (x) S F (D)\}] = \{v \| \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v\}$
49	43 47 48	syl2anc	$⊢ φ \to F [\{x \in C \| F (x) S F (D)\}] = \{v \| \exists u \in \{x \in C \| F (x) S F (D)\} F (u) = v\}$
50	41 49	eqtr4d	$⊢ φ \to Pred (S, F [C], F (D)) = F [\{x \in C \| F (x) S F (D)\}]$
51		dfpred3g	$⊢ D \in A \to Pred (R, C, D) = \{x \in C \| x R D\}$
52	4 51	syl	$⊢ φ \to Pred (R, C, D) = \{x \in C \| x R D\}$
53	3	sselda	$⊢ (φ \land x \in C) \to x \in A$
54	2	r19.21bi	$⊢ (φ \land x \in A) \to \forall y \in A (x R y \leftrightarrow F (x) S F (y))$
55		breq2	$⊢ y = D \to (x R y \leftrightarrow x R D)$
56		fveq2	$⊢ y = D \to F (y) = F (D)$
57	56	breq2d	$⊢ y = D \to (F (x) S F (y) \leftrightarrow F (x) S F (D))$
58	55 57	bibi12d	$⊢ y = D \to ((x R y \leftrightarrow F (x) S F (y)) \leftrightarrow (x R D \leftrightarrow F (x) S F (D)))$
59	58	rspcv	$⊢ D \in A \to (\forall y \in A (x R y \leftrightarrow F (x) S F (y)) \to (x R D \leftrightarrow F (x) S F (D)))$
60	4 59	syl	$⊢ φ \to (\forall y \in A (x R y \leftrightarrow F (x) S F (y)) \to (x R D \leftrightarrow F (x) S F (D)))$
61	60	adantr	$⊢ (φ \land x \in A) \to (\forall y \in A (x R y \leftrightarrow F (x) S F (y)) \to (x R D \leftrightarrow F (x) S F (D)))$
62	54 61	mpd	$⊢ (φ \land x \in A) \to (x R D \leftrightarrow F (x) S F (D))$
63	53 62	syldan	$⊢ (φ \land x \in C) \to (x R D \leftrightarrow F (x) S F (D))$
64	63	rabbidva	$⊢ φ \to \{x \in C \| x R D\} = \{x \in C \| F (x) S F (D)\}$
65	52 64	eqtrd	$⊢ φ \to Pred (R, C, D) = \{x \in C \| F (x) S F (D)\}$
66	65	imaeq2d	$⊢ φ \to F [Pred (R, C, D)] = F [\{x \in C \| F (x) S F (D)\}]$
67	50 66	eqtr4d	$⊢ φ \to Pred (S, F [C], F (D)) = F [Pred (R, C, D)]$

Metamath Proof Explorer

Theorem fnrelpredd

Proof