wfrlem17

Description: Without using ax-rep , show that all restrictions of wrecs are sets. (Contributed by Scott Fenton, 31-Jul-2020)

	Ref	Expression
Hypotheses	wfrlem17.1	$⊢ R We A$
	wfrlem17.2	$⊢ R Se A$
	wfrlem17.3	$⊢ F = wrecs (R, A, G)$
Assertion	wfrlem17	$⊢ X \in dom F \to {F ↾}_{Pred (R, A, X)} \in V$

Proof

Step	Hyp	Ref	Expression
1		wfrlem17.1	$⊢ R We A$
2		wfrlem17.2	$⊢ R Se A$
3		wfrlem17.3	$⊢ F = wrecs (R, A, G)$
4	1 2 3	wfrfun	$⊢ Fun F$
5		funfvop	$⊢ (Fun F \land X \in dom F) \to ⟨X, F (X)⟩ \in F$
6	4 5	mpan	$⊢ X \in dom F \to ⟨X, F (X)⟩ \in F$
7		df-wrecs	$⊢ wrecs (R, A, G) = ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
8	3 7	eqtri	$⊢ F = ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
9	8	eleq2i	$⊢ ⟨X, F (X)⟩ \in F \leftrightarrow ⟨X, F (X)⟩ \in ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
10		eluni	$⊢ ⟨X, F (X)⟩ \in ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} \leftrightarrow \exists g (⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\})$
11	9 10	bitri	$⊢ ⟨X, F (X)⟩ \in F \leftrightarrow \exists g (⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\})$
12	6 11	sylib	$⊢ X \in dom F \to \exists g (⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\})$
13		simprr	$⊢ (X \in dom F \land (⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\})) \to g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
14		eqid	$⊢ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
15		vex	$⊢ g \in V$
16	14 15	wfrlem3a	$⊢ g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} \leftrightarrow \exists z (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = G ({g ↾}_{Pred (R, A, w)}))$
17	13 16	sylib	$⊢ (X \in dom F \land (⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\})) \to \exists z (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = G ({g ↾}_{Pred (R, A, w)}))$
18		3simpa	$⊢ (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = G ({g ↾}_{Pred (R, A, w)})) \to (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z))$
19		simprlr	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
20		elssuni	$⊢ g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} \to g \subseteq ⋃ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}$
21	20 8	sseqtrrdi	$⊢ g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\} \to g \subseteq F$
22	19 21	syl	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to g \subseteq F$
23		predeq3	$⊢ w = X \to Pred (R, A, w) = Pred (R, A, X)$
24	23	sseq1d	$⊢ w = X \to (Pred (R, A, w) \subseteq z \leftrightarrow Pred (R, A, X) \subseteq z)$
25		simprrr	$⊢ ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z))) \to \forall w \in z Pred (R, A, w) \subseteq z$
26	25	adantl	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to \forall w \in z Pred (R, A, w) \subseteq z$
27		simprll	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to ⟨X, F (X)⟩ \in g$
28		df-br	$⊢ X g F (X) \leftrightarrow ⟨X, F (X)⟩ \in g$
29	27 28	sylibr	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to X g F (X)$
30		fvex	$⊢ F (X) \in V$
31		breldmg	$⊢ (X \in dom F \land F (X) \in V \land X g F (X)) \to X \in dom g$
32	30 31	mp3an2	$⊢ (X \in dom F \land X g F (X)) \to X \in dom g$
33	29 32	syldan	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to X \in dom g$
34		simprrl	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to g Fn z$
35	34	fndmd	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to dom g = z$
36	33 35	eleqtrd	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to X \in z$
37	24 26 36	rspcdva	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to Pred (R, A, X) \subseteq z$
38	37 35	sseqtrrd	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to Pred (R, A, X) \subseteq dom g$
39		fun2ssres	$⊢ (Fun F \land g \subseteq F \land Pred (R, A, X) \subseteq dom g) \to {F ↾}_{Pred (R, A, X)} = {g ↾}_{Pred (R, A, X)}$
40	4 22 38 39	mp3an2i	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to {F ↾}_{Pred (R, A, X)} = {g ↾}_{Pred (R, A, X)}$
41	15	resex	$⊢ {g ↾}_{Pred (R, A, X)} \in V$
42	40 41	eqeltrdi	$⊢ (X \in dom F \land ((⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)))) \to {F ↾}_{Pred (R, A, X)} \in V$
43	42	expr	$⊢ (X \in dom F \land (⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\})) \to ((g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z)) \to {F ↾}_{Pred (R, A, X)} \in V)$
44	18 43	syl5	$⊢ (X \in dom F \land (⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\})) \to ((g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = G ({g ↾}_{Pred (R, A, w)})) \to {F ↾}_{Pred (R, A, X)} \in V)$
45	44	exlimdv	$⊢ (X \in dom F \land (⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\})) \to (\exists z (g Fn z \land (z \subseteq A \land \forall w \in z Pred (R, A, w) \subseteq z) \land \forall w \in z g (w) = G ({g ↾}_{Pred (R, A, w)})) \to {F ↾}_{Pred (R, A, X)} \in V)$
46	17 45	mpd	$⊢ (X \in dom F \land (⟨X, F (X)⟩ \in g \land g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}))\})) \to {F ↾}_{Pred (R, A, X)} \in V$
47	12 46	exlimddv	$⊢ X \in dom F \to {F ↾}_{Pred (R, A, X)} \in V$

Metamath Proof Explorer

Theorem wfrlem17

Proof