fnwe2lem3

Description: Lemma for fnwe2 . An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus T is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015)

	Ref	Expression
Hypotheses	fnwe2.su	$⊢ z = F (x) \to S = U$
	fnwe2.t	$⊢ T = \{⟨x, y⟩ \| (F (x) R F (y) \lor (F (x) = F (y) \land x U y))\}$
	fnwe2.s	$⊢ (φ \land x \in A) \to U We \{y \in A \| F (y) = F (x)\}$
	fnwe2.f	$⊢ φ \to ({F ↾}_{A}) : A ⟶ B$
	fnwe2.r	$⊢ φ \to R We B$
	fnwe2lem3.a	$⊢ φ \to a \subseteq A$
	fnwe2lem3.n0	$⊢ φ \to a \neq \emptyset$
Assertion	fnwe2lem3	$⊢ φ \to \exists b \in a \forall c \in a \neg c T b$

Proof

Step	Hyp	Ref	Expression
1		fnwe2.su	$⊢ z = F (x) \to S = U$
2		fnwe2.t	$⊢ T = \{⟨x, y⟩ \| (F (x) R F (y) \lor (F (x) = F (y) \land x U y))\}$
3		fnwe2.s	$⊢ (φ \land x \in A) \to U We \{y \in A \| F (y) = F (x)\}$
4		fnwe2.f	$⊢ φ \to ({F ↾}_{A}) : A ⟶ B$
5		fnwe2.r	$⊢ φ \to R We B$
6		fnwe2lem3.a	$⊢ φ \to a \subseteq A$
7		fnwe2lem3.n0	$⊢ φ \to a \neq \emptyset$
8		ffun	$⊢ ({F ↾}_{A}) : A ⟶ B \to Fun ({F ↾}_{A})$
9		vex	$⊢ a \in V$
10	9	funimaex	$⊢ Fun ({F ↾}_{A}) \to ({F ↾}_{A}) [a] \in V$
11	4 8 10	3syl	$⊢ φ \to ({F ↾}_{A}) [a] \in V$
12		wefr	$⊢ R We B \to R Fr B$
13	5 12	syl	$⊢ φ \to R Fr B$
14	4	fimassd	$⊢ φ \to ({F ↾}_{A}) [a] \subseteq B$
15	4	ffnd	$⊢ φ \to ({F ↾}_{A}) Fn A$
16		fnimaeq0	$⊢ (({F ↾}_{A}) Fn A \land a \subseteq A) \to (({F ↾}_{A}) [a] = \emptyset \leftrightarrow a = \emptyset)$
17	15 6 16	syl2anc	$⊢ φ \to (({F ↾}_{A}) [a] = \emptyset \leftrightarrow a = \emptyset)$
18	17	necon3bid	$⊢ φ \to (({F ↾}_{A}) [a] \neq \emptyset \leftrightarrow a \neq \emptyset)$
19	7 18	mpbird	$⊢ φ \to ({F ↾}_{A}) [a] \neq \emptyset$
20		fri	$⊢ ((({F ↾}_{A}) [a] \in V \land R Fr B) \land (({F ↾}_{A}) [a] \subseteq B \land ({F ↾}_{A}) [a] \neq \emptyset)) \to \exists d \in ({F ↾}_{A}) [a] \forall e \in ({F ↾}_{A}) [a] \neg e R d$
21	11 13 14 19 20	syl22anc	$⊢ φ \to \exists d \in ({F ↾}_{A}) [a] \forall e \in ({F ↾}_{A}) [a] \neg e R d$
22		df-ima	$⊢ ({F ↾}_{A}) [a] = ran ({({F ↾}_{A}) ↾}_{a})$
23	22	rexeqi	$⊢ \exists d \in ({F ↾}_{A}) [a] \forall e \in ({F ↾}_{A}) [a] \neg e R d \leftrightarrow \exists d \in ran ({({F ↾}_{A}) ↾}_{a}) \forall e \in ({F ↾}_{A}) [a] \neg e R d$
24	15 6	fnssresd	$⊢ φ \to ({({F ↾}_{A}) ↾}_{a}) Fn a$
25		breq2	$⊢ d = ({({F ↾}_{A}) ↾}_{a}) (f) \to (e R d \leftrightarrow e R ({({F ↾}_{A}) ↾}_{a}) (f))$
26	25	notbid	$⊢ d = ({({F ↾}_{A}) ↾}_{a}) (f) \to (\neg e R d \leftrightarrow \neg e R ({({F ↾}_{A}) ↾}_{a}) (f))$
27	26	ralbidv	$⊢ d = ({({F ↾}_{A}) ↾}_{a}) (f) \to (\forall e \in ({F ↾}_{A}) [a] \neg e R d \leftrightarrow \forall e \in ({F ↾}_{A}) [a] \neg e R ({({F ↾}_{A}) ↾}_{a}) (f))$
28	27	rexrn	$⊢ ({({F ↾}_{A}) ↾}_{a}) Fn a \to (\exists d \in ran ({({F ↾}_{A}) ↾}_{a}) \forall e \in ({F ↾}_{A}) [a] \neg e R d \leftrightarrow \exists f \in a \forall e \in ({F ↾}_{A}) [a] \neg e R ({({F ↾}_{A}) ↾}_{a}) (f))$
29	24 28	syl	$⊢ φ \to (\exists d \in ran ({({F ↾}_{A}) ↾}_{a}) \forall e \in ({F ↾}_{A}) [a] \neg e R d \leftrightarrow \exists f \in a \forall e \in ({F ↾}_{A}) [a] \neg e R ({({F ↾}_{A}) ↾}_{a}) (f))$
30	23 29	bitrid	$⊢ φ \to (\exists d \in ({F ↾}_{A}) [a] \forall e \in ({F ↾}_{A}) [a] \neg e R d \leftrightarrow \exists f \in a \forall e \in ({F ↾}_{A}) [a] \neg e R ({({F ↾}_{A}) ↾}_{a}) (f))$
31	22	raleqi	$⊢ \forall e \in ({F ↾}_{A}) [a] \neg e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \forall e \in ran ({({F ↾}_{A}) ↾}_{a}) \neg e R ({({F ↾}_{A}) ↾}_{a}) (f)$
32		breq1	$⊢ e = ({({F ↾}_{A}) ↾}_{a}) (d) \to (e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow ({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f))$
33	32	notbid	$⊢ e = ({({F ↾}_{A}) ↾}_{a}) (d) \to (\neg e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \neg ({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f))$
34	33	ralrn	$⊢ ({({F ↾}_{A}) ↾}_{a}) Fn a \to (\forall e \in ran ({({F ↾}_{A}) ↾}_{a}) \neg e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \forall d \in a \neg ({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f))$
35	24 34	syl	$⊢ φ \to (\forall e \in ran ({({F ↾}_{A}) ↾}_{a}) \neg e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \forall d \in a \neg ({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f))$
36	31 35	bitrid	$⊢ φ \to (\forall e \in ({F ↾}_{A}) [a] \neg e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \forall d \in a \neg ({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f))$
37	36	adantr	$⊢ (φ \land f \in a) \to (\forall e \in ({F ↾}_{A}) [a] \neg e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \forall d \in a \neg ({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f))$
38	6	resabs1d	$⊢ φ \to {({F ↾}_{A}) ↾}_{a} = {F ↾}_{a}$
39	38	ad2antrr	$⊢ ((φ \land f \in a) \land d \in a) \to {({F ↾}_{A}) ↾}_{a} = {F ↾}_{a}$
40	39	fveq1d	$⊢ ((φ \land f \in a) \land d \in a) \to ({({F ↾}_{A}) ↾}_{a}) (d) = ({F ↾}_{a}) (d)$
41		fvres	$⊢ d \in a \to ({F ↾}_{a}) (d) = F (d)$
42	41	adantl	$⊢ ((φ \land f \in a) \land d \in a) \to ({F ↾}_{a}) (d) = F (d)$
43	40 42	eqtrd	$⊢ ((φ \land f \in a) \land d \in a) \to ({({F ↾}_{A}) ↾}_{a}) (d) = F (d)$
44	39	fveq1d	$⊢ ((φ \land f \in a) \land d \in a) \to ({({F ↾}_{A}) ↾}_{a}) (f) = ({F ↾}_{a}) (f)$
45		fvres	$⊢ f \in a \to ({F ↾}_{a}) (f) = F (f)$
46	45	ad2antlr	$⊢ ((φ \land f \in a) \land d \in a) \to ({F ↾}_{a}) (f) = F (f)$
47	44 46	eqtrd	$⊢ ((φ \land f \in a) \land d \in a) \to ({({F ↾}_{A}) ↾}_{a}) (f) = F (f)$
48	43 47	breq12d	$⊢ ((φ \land f \in a) \land d \in a) \to (({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow F (d) R F (f))$
49	48	notbid	$⊢ ((φ \land f \in a) \land d \in a) \to (\neg ({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \neg F (d) R F (f))$
50	49	ralbidva	$⊢ (φ \land f \in a) \to (\forall d \in a \neg ({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \forall d \in a \neg F (d) R F (f))$
51	37 50	bitrd	$⊢ (φ \land f \in a) \to (\forall e \in ({F ↾}_{A}) [a] \neg e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \forall d \in a \neg F (d) R F (f))$
52	51	rexbidva	$⊢ φ \to (\exists f \in a \forall e \in ({F ↾}_{A}) [a] \neg e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow \exists f \in a \forall d \in a \neg F (d) R F (f))$
53	30 52	bitrd	$⊢ φ \to (\exists d \in ({F ↾}_{A}) [a] \forall e \in ({F ↾}_{A}) [a] \neg e R d \leftrightarrow \exists f \in a \forall d \in a \neg F (d) R F (f))$
54	9	inex1	$⊢ a \cap \{y \in A \| F (y) = F (f)\} \in V$
55	54	a1i	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to a \cap \{y \in A \| F (y) = F (f)\} \in V$
56	6	sselda	$⊢ (φ \land f \in a) \to f \in A$
57	1 2 3	fnwe2lem2	$⊢ (φ \land f \in A) \to ⦋ F (f) / z ⦌ S We \{y \in A \| F (y) = F (f)\}$
58		wefr	$⊢ ⦋ F (f) / z ⦌ S We \{y \in A \| F (y) = F (f)\} \to ⦋ F (f) / z ⦌ S Fr \{y \in A \| F (y) = F (f)\}$
59	57 58	syl	$⊢ (φ \land f \in A) \to ⦋ F (f) / z ⦌ S Fr \{y \in A \| F (y) = F (f)\}$
60	56 59	syldan	$⊢ (φ \land f \in a) \to ⦋ F (f) / z ⦌ S Fr \{y \in A \| F (y) = F (f)\}$
61	60	adantrr	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to ⦋ F (f) / z ⦌ S Fr \{y \in A \| F (y) = F (f)\}$
62		inss2	$⊢ a \cap \{y \in A \| F (y) = F (f)\} \subseteq \{y \in A \| F (y) = F (f)\}$
63	62	a1i	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to a \cap \{y \in A \| F (y) = F (f)\} \subseteq \{y \in A \| F (y) = F (f)\}$
64		simprl	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to f \in a$
65		fveqeq2	$⊢ y = f \to (F (y) = F (f) \leftrightarrow F (f) = F (f))$
66	56	adantrr	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to f \in A$
67		eqidd	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to F (f) = F (f)$
68	65 66 67	elrabd	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to f \in \{y \in A \| F (y) = F (f)\}$
69	64 68	elind	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to f \in (a \cap \{y \in A \| F (y) = F (f)\})$
70	69	ne0d	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to a \cap \{y \in A \| F (y) = F (f)\} \neq \emptyset$
71		fri	$⊢ ((a \cap \{y \in A \| F (y) = F (f)\} \in V \land ⦋ F (f) / z ⦌ S Fr \{y \in A \| F (y) = F (f)\}) \land (a \cap \{y \in A \| F (y) = F (f)\} \subseteq \{y \in A \| F (y) = F (f)\} \land a \cap \{y \in A \| F (y) = F (f)\} \neq \emptyset)) \to \exists e \in (a \cap \{y \in A \| F (y) = F (f)\}) \forall g \in (a \cap \{y \in A \| F (y) = F (f)\}) \neg g ⦋ F (f) / z ⦌ S e$
72	55 61 63 70 71	syl22anc	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to \exists e \in (a \cap \{y \in A \| F (y) = F (f)\}) \forall g \in (a \cap \{y \in A \| F (y) = F (f)\}) \neg g ⦋ F (f) / z ⦌ S e$
73		elin	$⊢ e \in (a \cap \{y \in A \| F (y) = F (f)\}) \leftrightarrow (e \in a \land e \in \{y \in A \| F (y) = F (f)\})$
74		fveqeq2	$⊢ y = e \to (F (y) = F (f) \leftrightarrow F (e) = F (f))$
75	74	elrab	$⊢ e \in \{y \in A \| F (y) = F (f)\} \leftrightarrow (e \in A \land F (e) = F (f))$
76	75	anbi2i	$⊢ (e \in a \land e \in \{y \in A \| F (y) = F (f)\}) \leftrightarrow (e \in a \land (e \in A \land F (e) = F (f)))$
77	73 76	bitri	$⊢ e \in (a \cap \{y \in A \| F (y) = F (f)\}) \leftrightarrow (e \in a \land (e \in A \land F (e) = F (f)))$
78		elin	$⊢ g \in (a \cap \{y \in A \| F (y) = F (f)\}) \leftrightarrow (g \in a \land g \in \{y \in A \| F (y) = F (f)\})$
79		fveqeq2	$⊢ y = g \to (F (y) = F (f) \leftrightarrow F (g) = F (f))$
80	79	elrab	$⊢ g \in \{y \in A \| F (y) = F (f)\} \leftrightarrow (g \in A \land F (g) = F (f))$
81	80	anbi2i	$⊢ (g \in a \land g \in \{y \in A \| F (y) = F (f)\}) \leftrightarrow (g \in a \land (g \in A \land F (g) = F (f)))$
82	78 81	bitri	$⊢ g \in (a \cap \{y \in A \| F (y) = F (f)\}) \leftrightarrow (g \in a \land (g \in A \land F (g) = F (f)))$
83	82	imbi1i	$⊢ (g \in (a \cap \{y \in A \| F (y) = F (f)\}) \to \neg g ⦋ F (f) / z ⦌ S e) \leftrightarrow ((g \in a \land (g \in A \land F (g) = F (f))) \to \neg g ⦋ F (f) / z ⦌ S e)$
84		impexp	$⊢ ((g \in a \land (g \in A \land F (g) = F (f))) \to \neg g ⦋ F (f) / z ⦌ S e) \leftrightarrow (g \in a \to ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e))$
85	83 84	bitri	$⊢ (g \in (a \cap \{y \in A \| F (y) = F (f)\}) \to \neg g ⦋ F (f) / z ⦌ S e) \leftrightarrow (g \in a \to ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e))$
86	85	ralbii2	$⊢ \forall g \in (a \cap \{y \in A \| F (y) = F (f)\}) \neg g ⦋ F (f) / z ⦌ S e \leftrightarrow \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)$
87		breq2	$⊢ b = e \to (c T b \leftrightarrow c T e)$
88	87	notbid	$⊢ b = e \to (\neg c T b \leftrightarrow \neg c T e)$
89	88	ralbidv	$⊢ b = e \to (\forall c \in a \neg c T b \leftrightarrow \forall c \in a \neg c T e)$
90		simplrl	$⊢ (((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \to e \in a$
91		fveq2	$⊢ d = c \to F (d) = F (c)$
92	91	breq1d	$⊢ d = c \to (F (d) R F (f) \leftrightarrow F (c) R F (f))$
93	92	notbid	$⊢ d = c \to (\neg F (d) R F (f) \leftrightarrow \neg F (c) R F (f))$
94		simplrr	$⊢ ((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \to \forall d \in a \neg F (d) R F (f)$
95	94	ad2antrr	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to \forall d \in a \neg F (d) R F (f)$
96		simpr	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to c \in a$
97	93 95 96	rspcdva	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to \neg F (c) R F (f)$
98		simprrr	$⊢ ((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \to F (e) = F (f)$
99	98	ad2antrr	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to F (e) = F (f)$
100	99	breq2d	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to (F (c) R F (e) \leftrightarrow F (c) R F (f))$
101	97 100	mtbird	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to \neg F (c) R F (e)$
102	6	ad3antrrr	$⊢ (((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \to a \subseteq A$
103	102	sselda	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to c \in A$
104	103	adantrr	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to c \in A$
105		simprr	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to F (c) = F (e)$
106	98	ad2antrr	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to F (e) = F (f)$
107	105 106	eqtrd	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to F (c) = F (f)$
108		eleq1w	$⊢ g = c \to (g \in A \leftrightarrow c \in A)$
109		fveqeq2	$⊢ g = c \to (F (g) = F (f) \leftrightarrow F (c) = F (f))$
110	108 109	anbi12d	$⊢ g = c \to ((g \in A \land F (g) = F (f)) \leftrightarrow (c \in A \land F (c) = F (f)))$
111		breq1	$⊢ g = c \to (g ⦋ F (f) / z ⦌ S e \leftrightarrow c ⦋ F (f) / z ⦌ S e)$
112	111	notbid	$⊢ g = c \to (\neg g ⦋ F (f) / z ⦌ S e \leftrightarrow \neg c ⦋ F (f) / z ⦌ S e)$
113	110 112	imbi12d	$⊢ g = c \to (((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e) \leftrightarrow ((c \in A \land F (c) = F (f)) \to \neg c ⦋ F (f) / z ⦌ S e))$
114		simplr	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)$
115		simprl	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to c \in a$
116	113 114 115	rspcdva	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to ((c \in A \land F (c) = F (f)) \to \neg c ⦋ F (f) / z ⦌ S e)$
117	104 107 116	mp2and	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to \neg c ⦋ F (f) / z ⦌ S e$
118	105 106	eqtr2d	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to F (f) = F (c)$
119	118	csbeq1d	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to ⦋ F (f) / z ⦌ S = ⦋ F (c) / z ⦌ S$
120	119	breqd	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to (c ⦋ F (f) / z ⦌ S e \leftrightarrow c ⦋ F (c) / z ⦌ S e)$
121	117 120	mtbid	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land (c \in a \land F (c) = F (e))) \to \neg c ⦋ F (c) / z ⦌ S e$
122	121	expr	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to (F (c) = F (e) \to \neg c ⦋ F (c) / z ⦌ S e)$
123		imnan	$⊢ (F (c) = F (e) \to \neg c ⦋ F (c) / z ⦌ S e) \leftrightarrow \neg (F (c) = F (e) \land c ⦋ F (c) / z ⦌ S e)$
124	122 123	sylib	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to \neg (F (c) = F (e) \land c ⦋ F (c) / z ⦌ S e)$
125		ioran	$⊢ \neg (F (c) R F (e) \lor (F (c) = F (e) \land c ⦋ F (c) / z ⦌ S e)) \leftrightarrow (\neg F (c) R F (e) \land \neg (F (c) = F (e) \land c ⦋ F (c) / z ⦌ S e))$
126	101 124 125	sylanbrc	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to \neg (F (c) R F (e) \lor (F (c) = F (e) \land c ⦋ F (c) / z ⦌ S e))$
127	1 2	fnwe2lem1	$⊢ c T e \leftrightarrow (F (c) R F (e) \lor (F (c) = F (e) \land c ⦋ F (c) / z ⦌ S e))$
128	126 127	sylnibr	$⊢ ((((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \land c \in a) \to \neg c T e$
129	128	ralrimiva	$⊢ (((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \to \forall c \in a \neg c T e$
130	89 90 129	rspcedvdw	$⊢ (((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \land \forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e)) \to \exists b \in a \forall c \in a \neg c T b$
131	130	ex	$⊢ ((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \to (\forall g \in a ((g \in A \land F (g) = F (f)) \to \neg g ⦋ F (f) / z ⦌ S e) \to \exists b \in a \forall c \in a \neg c T b)$
132	86 131	biimtrid	$⊢ ((φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \land (e \in a \land (e \in A \land F (e) = F (f)))) \to (\forall g \in (a \cap \{y \in A \| F (y) = F (f)\}) \neg g ⦋ F (f) / z ⦌ S e \to \exists b \in a \forall c \in a \neg c T b)$
133	132	ex	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to ((e \in a \land (e \in A \land F (e) = F (f))) \to (\forall g \in (a \cap \{y \in A \| F (y) = F (f)\}) \neg g ⦋ F (f) / z ⦌ S e \to \exists b \in a \forall c \in a \neg c T b))$
134	77 133	biimtrid	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to (e \in (a \cap \{y \in A \| F (y) = F (f)\}) \to (\forall g \in (a \cap \{y \in A \| F (y) = F (f)\}) \neg g ⦋ F (f) / z ⦌ S e \to \exists b \in a \forall c \in a \neg c T b))$
135	134	rexlimdv	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to (\exists e \in (a \cap \{y \in A \| F (y) = F (f)\}) \forall g \in (a \cap \{y \in A \| F (y) = F (f)\}) \neg g ⦋ F (f) / z ⦌ S e \to \exists b \in a \forall c \in a \neg c T b)$
136	72 135	mpd	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to \exists b \in a \forall c \in a \neg c T b$
137	136	rexlimdvaa	$⊢ φ \to (\exists f \in a \forall d \in a \neg F (d) R F (f) \to \exists b \in a \forall c \in a \neg c T b)$
138	53 137	sylbid	$⊢ φ \to (\exists d \in ({F ↾}_{A}) [a] \forall e \in ({F ↾}_{A}) [a] \neg e R d \to \exists b \in a \forall c \in a \neg c T b)$
139	21 138	mpd	$⊢ φ \to \exists b \in a \forall c \in a \neg c T b$

Metamath Proof Explorer

Theorem fnwe2lem3

Proof