relpfrlem

Description: Lemma for relpfr . Proved without using the Axiom of Replacement. This is isofrlem with weaker hypotheses. (Contributed by Eric Schmidt, 11-Oct-2025)

	Ref	Expression
Hypotheses	relpfrlem.1	No typesetting found for \|- ( ph -> H RelPres R , S ( A , B ) ) with typecode \|-
	relpfrlem.2	$⊢ φ \to H [x] \in V$
Assertion	relpfrlem	$⊢ φ \to (S Fr B \to R Fr A)$

Proof

Step	Hyp	Ref	Expression
1		relpfrlem.1	Could not format ( ph -> H RelPres R , S ( A , B ) ) : No typesetting found for \|- ( ph -> H RelPres R , S ( A , B ) ) with typecode \|-
2		relpfrlem.2	$⊢ φ \to H [x] \in V$
3		relpf	Could not format ( H RelPres R , S ( A , B ) -> H : A --> B ) : No typesetting found for \|- ( H RelPres R , S ( A , B ) -> H : A --> B ) with typecode \|-
4	1 3	syl	$⊢ φ \to H : A ⟶ B$
5		ffn	$⊢ H : A ⟶ B \to H Fn A$
6		n0	$⊢ x \neq \emptyset \leftrightarrow \exists y y \in x$
7		fnfvima	$⊢ (H Fn A \land x \subseteq A \land y \in x) \to H (y) \in H [x]$
8	7	ne0d	$⊢ (H Fn A \land x \subseteq A \land y \in x) \to H [x] \neq \emptyset$
9	8	3expia	$⊢ (H Fn A \land x \subseteq A) \to (y \in x \to H [x] \neq \emptyset)$
10	9	exlimdv	$⊢ (H Fn A \land x \subseteq A) \to (\exists y y \in x \to H [x] \neq \emptyset)$
11	6 10	biimtrid	$⊢ (H Fn A \land x \subseteq A) \to (x \neq \emptyset \to H [x] \neq \emptyset)$
12	11	expimpd	$⊢ H Fn A \to ((x \subseteq A \land x \neq \emptyset) \to H [x] \neq \emptyset)$
13	5 12	syl	$⊢ H : A ⟶ B \to ((x \subseteq A \land x \neq \emptyset) \to H [x] \neq \emptyset)$
14		fimass	$⊢ H : A ⟶ B \to H [x] \subseteq B$
15	13 14	jctild	$⊢ H : A ⟶ B \to ((x \subseteq A \land x \neq \emptyset) \to (H [x] \subseteq B \land H [x] \neq \emptyset))$
16	4 15	syl	$⊢ φ \to ((x \subseteq A \land x \neq \emptyset) \to (H [x] \subseteq B \land H [x] \neq \emptyset))$
17		dffr3	$⊢ S Fr B \leftrightarrow \forall z ((z \subseteq B \land z \neq \emptyset) \to \exists w \in z z \cap S^{-1} [\{w\}] = \emptyset)$
18		sseq1	$⊢ z = H [x] \to (z \subseteq B \leftrightarrow H [x] \subseteq B)$
19		neeq1	$⊢ z = H [x] \to (z \neq \emptyset \leftrightarrow H [x] \neq \emptyset)$
20	18 19	anbi12d	$⊢ z = H [x] \to ((z \subseteq B \land z \neq \emptyset) \leftrightarrow (H [x] \subseteq B \land H [x] \neq \emptyset))$
21		ineq1	$⊢ z = H [x] \to z \cap S^{-1} [\{w\}] = H [x] \cap S^{-1} [\{w\}]$
22	21	eqeq1d	$⊢ z = H [x] \to (z \cap S^{-1} [\{w\}] = \emptyset \leftrightarrow H [x] \cap S^{-1} [\{w\}] = \emptyset)$
23	22	rexeqbi1dv	$⊢ z = H [x] \to (\exists w \in z z \cap S^{-1} [\{w\}] = \emptyset \leftrightarrow \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset)$
24	20 23	imbi12d	$⊢ z = H [x] \to (((z \subseteq B \land z \neq \emptyset) \to \exists w \in z z \cap S^{-1} [\{w\}] = \emptyset) \leftrightarrow ((H [x] \subseteq B \land H [x] \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
25	24	spcgv	$⊢ H [x] \in V \to (\forall z ((z \subseteq B \land z \neq \emptyset) \to \exists w \in z z \cap S^{-1} [\{w\}] = \emptyset) \to ((H [x] \subseteq B \land H [x] \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
26	2 25	syl	$⊢ φ \to (\forall z ((z \subseteq B \land z \neq \emptyset) \to \exists w \in z z \cap S^{-1} [\{w\}] = \emptyset) \to ((H [x] \subseteq B \land H [x] \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
27	17 26	biimtrid	$⊢ φ \to (S Fr B \to ((H [x] \subseteq B \land H [x] \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
28	16 27	syl5d	$⊢ φ \to (S Fr B \to ((x \subseteq A \land x \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
29	4	adantr	$⊢ (φ \land x \subseteq A) \to H : A ⟶ B$
30	29	ffund	$⊢ (φ \land x \subseteq A) \to Fun H$
31		simpl	$⊢ (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to w \in H [x]$
32		fvelima	$⊢ (Fun H \land w \in H [x]) \to \exists y \in x H (y) = w$
33	30 31 32	syl2an	$⊢ ((φ \land x \subseteq A) \land (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset)) \to \exists y \in x H (y) = w$
34		sneq	$⊢ w = H (y) \to \{w\} = \{H (y)\}$
35	34	eqcoms	$⊢ H (y) = w \to \{w\} = \{H (y)\}$
36	35	imaeq2d	$⊢ H (y) = w \to S^{-1} [\{w\}] = S^{-1} [\{H (y)\}]$
37	36	ineq2d	$⊢ H (y) = w \to H [x] \cap S^{-1} [\{w\}] = H [x] \cap S^{-1} [\{H (y)\}]$
38	37	eqeq1d	$⊢ H (y) = w \to (H [x] \cap S^{-1} [\{w\}] = \emptyset \leftrightarrow H [x] \cap S^{-1} [\{H (y)\}] = \emptyset)$
39	38	biimpd	$⊢ H (y) = w \to (H [x] \cap S^{-1} [\{w\}] = \emptyset \to H [x] \cap S^{-1} [\{H (y)\}] = \emptyset)$
40		ssel	$⊢ x \subseteq A \to (y \in x \to y \in A)$
41	40	imdistani	$⊢ (x \subseteq A \land y \in x) \to (x \subseteq A \land y \in A)$
42		relpmin	Could not format ( ( H RelPres R , S ( A , B ) /\ ( x C_ A /\ y e. A ) ) -> ( ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = (/) -> ( x i^i ( `' R " { y } ) ) = (/) ) ) : No typesetting found for \|- ( ( H RelPres R , S ( A , B ) /\ ( x C_ A /\ y e. A ) ) -> ( ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = (/) -> ( x i^i ( `' R " { y } ) ) = (/) ) ) with typecode \|-
43	1 41 42	syl2an	$⊢ (φ \land (x \subseteq A \land y \in x)) \to (H [x] \cap S^{-1} [\{H (y)\}] = \emptyset \to x \cap R^{-1} [\{y\}] = \emptyset)$
44	39 43	sylan9r	$⊢ ((φ \land (x \subseteq A \land y \in x)) \land H (y) = w) \to (H [x] \cap S^{-1} [\{w\}] = \emptyset \to x \cap R^{-1} [\{y\}] = \emptyset)$
45	44	adantld	$⊢ ((φ \land (x \subseteq A \land y \in x)) \land H (y) = w) \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to x \cap R^{-1} [\{y\}] = \emptyset)$
46	45	exp42	$⊢ φ \to (x \subseteq A \to (y \in x \to (H (y) = w \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to x \cap R^{-1} [\{y\}] = \emptyset))))$
47	46	imp	$⊢ (φ \land x \subseteq A) \to (y \in x \to (H (y) = w \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to x \cap R^{-1} [\{y\}] = \emptyset)))$
48	47	com3l	$⊢ y \in x \to (H (y) = w \to ((φ \land x \subseteq A) \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to x \cap R^{-1} [\{y\}] = \emptyset)))$
49	48	com4t	$⊢ (φ \land x \subseteq A) \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to (y \in x \to (H (y) = w \to x \cap R^{-1} [\{y\}] = \emptyset)))$
50	49	imp	$⊢ ((φ \land x \subseteq A) \land (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset)) \to (y \in x \to (H (y) = w \to x \cap R^{-1} [\{y\}] = \emptyset))$
51	50	reximdvai	$⊢ ((φ \land x \subseteq A) \land (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset)) \to (\exists y \in x H (y) = w \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$
52	33 51	mpd	$⊢ ((φ \land x \subseteq A) \land (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset)) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset$
53	52	rexlimdvaa	$⊢ (φ \land x \subseteq A) \to (\exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$
54	53	ex	$⊢ φ \to (x \subseteq A \to (\exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
55	54	adantrd	$⊢ φ \to ((x \subseteq A \land x \neq \emptyset) \to (\exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
56	55	a2d	$⊢ φ \to (((x \subseteq A \land x \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset) \to ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
57	28 56	syld	$⊢ φ \to (S Fr B \to ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
58	57	alrimdv	$⊢ φ \to (S Fr B \to \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
59		dffr3	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$
60	58 59	imbitrrdi	$⊢ φ \to (S Fr B \to R Fr A)$

Metamath Proof Explorer

Theorem relpfrlem

Proof