fnwe2lem2

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$
	fnwe2lem2.a	$⊢ φ \to a \subseteq A$
	fnwe2lem2.n0	$⊢ φ \to a \neq \emptyset$
Assertion	fnwe2lem2	$⊢ φ \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		fnwe2lem2.a	$⊢ φ \to a \subseteq A$
7		fnwe2lem2.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		imassrn	$⊢ ({F ↾}_{A}) [a] \subseteq ran ({F ↾}_{A})$
15	4	frnd	$⊢ φ \to ran ({F ↾}_{A}) \subseteq B$
16	14 15	sstrid	$⊢ φ \to ({F ↾}_{A}) [a] \subseteq B$
17		incom	$⊢ dom ({F ↾}_{A}) \cap a = a \cap dom ({F ↾}_{A})$
18	4	fdmd	$⊢ φ \to dom ({F ↾}_{A}) = A$
19	6 18	sseqtrrd	$⊢ φ \to a \subseteq dom ({F ↾}_{A})$
20		df-ss	$⊢ a \subseteq dom ({F ↾}_{A}) \leftrightarrow a \cap dom ({F ↾}_{A}) = a$
21	19 20	sylib	$⊢ φ \to a \cap dom ({F ↾}_{A}) = a$
22	17 21	syl5eq	$⊢ φ \to dom ({F ↾}_{A}) \cap a = a$
23	22 7	eqnetrd	$⊢ φ \to dom ({F ↾}_{A}) \cap a \neq \emptyset$
24		imadisj	$⊢ ({F ↾}_{A}) [a] = \emptyset \leftrightarrow dom ({F ↾}_{A}) \cap a = \emptyset$
25	24	necon3bii	$⊢ ({F ↾}_{A}) [a] \neq \emptyset \leftrightarrow dom ({F ↾}_{A}) \cap a \neq \emptyset$
26	23 25	sylibr	$⊢ φ \to ({F ↾}_{A}) [a] \neq \emptyset$
27		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$
28	11 13 16 26 27	syl22anc	$⊢ φ \to \exists d \in ({F ↾}_{A}) [a] \forall e \in ({F ↾}_{A}) [a] \neg e R d$
29		df-ima	$⊢ ({F ↾}_{A}) [a] = ran ({({F ↾}_{A}) ↾}_{a})$
30	29	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$
31	4	ffnd	$⊢ φ \to ({F ↾}_{A}) Fn A$
32		fnssres	$⊢ (({F ↾}_{A}) Fn A \land a \subseteq A) \to ({({F ↾}_{A}) ↾}_{a}) Fn a$
33	31 6 32	syl2anc	$⊢ φ \to ({({F ↾}_{A}) ↾}_{a}) Fn a$
34		breq2	$⊢ d = ({({F ↾}_{A}) ↾}_{a}) (f) \to (e R d \leftrightarrow e R ({({F ↾}_{A}) ↾}_{a}) (f))$
35	34	notbid	$⊢ d = ({({F ↾}_{A}) ↾}_{a}) (f) \to (\neg e R d \leftrightarrow \neg e R ({({F ↾}_{A}) ↾}_{a}) (f))$
36	35	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))$
37	36	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))$
38	33 37	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))$
39	30 38	syl5bb	$⊢ φ \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))$
40	29	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)$
41		breq1	$⊢ e = ({({F ↾}_{A}) ↾}_{a}) (d) \to (e R ({({F ↾}_{A}) ↾}_{a}) (f) \leftrightarrow ({({F ↾}_{A}) ↾}_{a}) (d) R ({({F ↾}_{A}) ↾}_{a}) (f))$
42	41	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))$
43	42	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))$
44	33 43	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))$
45	40 44	syl5bb	$⊢ φ \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))$
46	45	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))$
47	6	resabs1d	$⊢ φ \to {({F ↾}_{A}) ↾}_{a} = {F ↾}_{a}$
48	47	ad2antrr	$⊢ ((φ \land f \in a) \land d \in a) \to {({F ↾}_{A}) ↾}_{a} = {F ↾}_{a}$
49	48	fveq1d	$⊢ ((φ \land f \in a) \land d \in a) \to ({({F ↾}_{A}) ↾}_{a}) (d) = ({F ↾}_{a}) (d)$
50		fvres	$⊢ d \in a \to ({F ↾}_{a}) (d) = F (d)$
51	50	adantl	$⊢ ((φ \land f \in a) \land d \in a) \to ({F ↾}_{a}) (d) = F (d)$
52	49 51	eqtrd	$⊢ ((φ \land f \in a) \land d \in a) \to ({({F ↾}_{A}) ↾}_{a}) (d) = F (d)$
53	48	fveq1d	$⊢ ((φ \land f \in a) \land d \in a) \to ({({F ↾}_{A}) ↾}_{a}) (f) = ({F ↾}_{a}) (f)$
54		fvres	$⊢ f \in a \to ({F ↾}_{a}) (f) = F (f)$
55	54	ad2antlr	$⊢ ((φ \land f \in a) \land d \in a) \to ({F ↾}_{a}) (f) = F (f)$
56	53 55	eqtrd	$⊢ ((φ \land f \in a) \land d \in a) \to ({({F ↾}_{A}) ↾}_{a}) (f) = F (f)$
57	52 56	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))$
58	57	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))$
59	58	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))$
60	46 59	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))$
61	60	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))$
62	39 61	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))$
63	9	inex1	$⊢ a \cap \{y \in A \| F (y) = F (f)\} \in V$
64	63	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$
65	6	sselda	$⊢ (φ \land f \in a) \to f \in A$
66	1 2 3	fnwe2lem1	$⊢ (φ \land f \in A) \to ⦋ F (f) / z ⦌ S We \{y \in A \| F (y) = F (f)\}$
67		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)\}$
68	66 67	syl	$⊢ (φ \land f \in A) \to ⦋ F (f) / z ⦌ S Fr \{y \in A \| F (y) = F (f)\}$
69	65 68	syldan	$⊢ (φ \land f \in a) \to ⦋ F (f) / z ⦌ S Fr \{y \in A \| F (y) = F (f)\}$
70	69	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)\}$
71		inss2	$⊢ a \cap \{y \in A \| F (y) = F (f)\} \subseteq \{y \in A \| F (y) = F (f)\}$
72	71	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)\}$
73		simprl	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to f \in a$
74		fveqeq2	$⊢ y = f \to (F (y) = F (f) \leftrightarrow F (f) = F (f))$
75	65	adantrr	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to f \in A$
76		eqidd	$⊢ (φ \land (f \in a \land \forall d \in a \neg F (d) R F (f))) \to F (f) = F (f)$
77	74 75 76	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)\}$
78	73 77	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)\})$
79	78	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$
80		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$
81	64 70 72 79 80	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$
82		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)\})$
83		fveqeq2	$⊢ y = e \to (F (y) = F (f) \leftrightarrow F (e) = F (f))$
84	83	elrab	$⊢ e \in \{y \in A \| F (y) = F (f)\} \leftrightarrow (e \in A \land F (e) = F (f))$
85	84	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)))$
86	82 85	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)))$
87		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)\})$
88		fveqeq2	$⊢ y = g \to (F (y) = F (f) \leftrightarrow F (g) = F (f))$
89	88	elrab	$⊢ g \in \{y \in A \| F (y) = F (f)\} \leftrightarrow (g \in A \land F (g) = F (f))$
90	89	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)))$
91	87 90	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)))$
92	91	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)$
93		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))$
94	92 93	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))$
95	94	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)$
96		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$
97		fveq2	$⊢ d = c \to F (d) = F (c)$
98	97	breq1d	$⊢ d = c \to (F (d) R F (f) \leftrightarrow F (c) R F (f))$
99	98	notbid	$⊢ d = c \to (\neg F (d) R F (f) \leftrightarrow \neg F (c) R F (f))$
100		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)$
101	100	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)$
102		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$
103	99 101 102	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)$
104		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)$
105	104	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)$
106	105	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))$
107	103 106	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)$
108	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$
109	108	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$
110	109	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$
111		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)$
112	104	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)$
113	111 112	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)$
114		eleq1w	$⊢ g = c \to (g \in A \leftrightarrow c \in A)$
115		fveqeq2	$⊢ g = c \to (F (g) = F (f) \leftrightarrow F (c) = F (f))$
116	114 115	anbi12d	$⊢ g = c \to ((g \in A \land F (g) = F (f)) \leftrightarrow (c \in A \land F (c) = F (f)))$
117		breq1	$⊢ g = c \to (g ⦋ F (f) / z ⦌ S e \leftrightarrow c ⦋ F (f) / z ⦌ S e)$
118	117	notbid	$⊢ g = c \to (\neg g ⦋ F (f) / z ⦌ S e \leftrightarrow \neg c ⦋ F (f) / z ⦌ S e)$
119	116 118	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))$
120		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)$
121		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$
122	119 120 121	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)$
123	110 113 122	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$
124	111 112	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)$
125	124	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$
126	125	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)$
127	123 126	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$
128	127	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)$
129		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)$
130	128 129	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)$
131		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))$
132	107 130 131	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))$
133	1 2	fnwe2val	$⊢ c T e \leftrightarrow (F (c) R F (e) \lor (F (c) = F (e) \land c ⦋ F (c) / z ⦌ S e))$
134	132 133	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$
135	134	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$
136		breq2	$⊢ b = e \to (c T b \leftrightarrow c T e)$
137	136	notbid	$⊢ b = e \to (\neg c T b \leftrightarrow \neg c T e)$
138	137	ralbidv	$⊢ b = e \to (\forall c \in a \neg c T b \leftrightarrow \forall c \in a \neg c T e)$
139	138	rspcev	$⊢ (e \in a \land \forall c \in a \neg c T e) \to \exists b \in a \forall c \in a \neg c T b$
140	96 135 139	syl2anc	$⊢ (((φ \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$
141	140	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)$
142	95 141	syl5bi	$⊢ ((φ \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)$
143	142	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))$
144	86 143	syl5bi	$⊢ (φ \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))$
145	144	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)$
146	81 145	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$
147	146	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)$
148	62 147	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)$
149	28 148	mpd	$⊢ φ \to \exists b \in a \forall c \in a \neg c T b$

Metamath Proof Explorer

Theorem fnwe2lem2

Proof