bnj1321

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1321.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1321.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1321.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1321.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
Assertion	bnj1321	$⊢ (R FrSe A \land \exists f τ) \to \exists! f τ$

Proof

Step	Hyp	Ref	Expression
1		bnj1321.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1321.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1321.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1321.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		simpr	$⊢ (R FrSe A \land \exists f τ) \to \exists f τ$
6		simp1	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to R FrSe A$
7	4	simplbi	$⊢ τ \to f \in C$
8	7	3ad2ant2	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to f \in C$
9		nfab1	$⊢ \underline{Ⅎ} f \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
10	3 9	nfcxfr	$⊢ \underline{Ⅎ} f C$
11	10	nfcri	$⊢ Ⅎ f g \in C$
12		nfv	$⊢ Ⅎ f dom g = \{x\} \cup trCl (x, A, R)$
13	11 12	nfan	$⊢ Ⅎ f (g \in C \land dom g = \{x\} \cup trCl (x, A, R))$
14		eleq1w	$⊢ f = g \to (f \in C \leftrightarrow g \in C)$
15		dmeq	$⊢ f = g \to dom f = dom g$
16	15	eqeq1d	$⊢ f = g \to (dom f = \{x\} \cup trCl (x, A, R) \leftrightarrow dom g = \{x\} \cup trCl (x, A, R))$
17	14 16	anbi12d	$⊢ f = g \to ((f \in C \land dom f = \{x\} \cup trCl (x, A, R)) \leftrightarrow (g \in C \land dom g = \{x\} \cup trCl (x, A, R)))$
18	4 17	syl5bb	$⊢ f = g \to (τ \leftrightarrow (g \in C \land dom g = \{x\} \cup trCl (x, A, R)))$
19	13 18	sbiev	$⊢ [g/ f] τ \leftrightarrow (g \in C \land dom g = \{x\} \cup trCl (x, A, R))$
20	19	simplbi	$⊢ [g/ f] τ \to g \in C$
21	20	3ad2ant3	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to g \in C$
22		eqid	$⊢ dom f \cap dom g = dom f \cap dom g$
23	1 2 3 22	bnj1326	$⊢ (R FrSe A \land f \in C \land g \in C) \to {f ↾}_{(dom f \cap dom g)} = {g ↾}_{(dom f \cap dom g)}$
24	6 8 21 23	syl3anc	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to {f ↾}_{(dom f \cap dom g)} = {g ↾}_{(dom f \cap dom g)}$
25	4	simprbi	$⊢ τ \to dom f = \{x\} \cup trCl (x, A, R)$
26	25	3ad2ant2	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to dom f = \{x\} \cup trCl (x, A, R)$
27	19	simprbi	$⊢ [g/ f] τ \to dom g = \{x\} \cup trCl (x, A, R)$
28	27	3ad2ant3	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to dom g = \{x\} \cup trCl (x, A, R)$
29	26 28	eqtr4d	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to dom f = dom g$
30		bnj1322	$⊢ dom f = dom g \to dom f \cap dom g = dom f$
31	30	reseq2d	$⊢ dom f = dom g \to {f ↾}_{(dom f \cap dom g)} = {f ↾}_{dom f}$
32	29 31	syl	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to {f ↾}_{(dom f \cap dom g)} = {f ↾}_{dom f}$
33		releq	$⊢ z = f \to (Rel z \leftrightarrow Rel f)$
34	1 2 3	bnj66	$⊢ z \in C \to Rel z$
35	33 34	vtoclga	$⊢ f \in C \to Rel f$
36		resdm	$⊢ Rel f \to {f ↾}_{dom f} = f$
37	8 35 36	3syl	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to {f ↾}_{dom f} = f$
38	32 37	eqtrd	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to {f ↾}_{(dom f \cap dom g)} = f$
39		eqeq2	$⊢ dom f = dom g \to (dom f \cap dom g = dom f \leftrightarrow dom f \cap dom g = dom g)$
40	30 39	mpbid	$⊢ dom f = dom g \to dom f \cap dom g = dom g$
41	40	reseq2d	$⊢ dom f = dom g \to {g ↾}_{(dom f \cap dom g)} = {g ↾}_{dom g}$
42	29 41	syl	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to {g ↾}_{(dom f \cap dom g)} = {g ↾}_{dom g}$
43	1 2 3	bnj66	$⊢ g \in C \to Rel g$
44		resdm	$⊢ Rel g \to {g ↾}_{dom g} = g$
45	21 43 44	3syl	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to {g ↾}_{dom g} = g$
46	42 45	eqtrd	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to {g ↾}_{(dom f \cap dom g)} = g$
47	24 38 46	3eqtr3d	$⊢ (R FrSe A \land τ \land [g/ f] τ) \to f = g$
48	47	3expib	$⊢ R FrSe A \to ((τ \land [g/ f] τ) \to f = g)$
49	48	alrimivv	$⊢ R FrSe A \to \forall f \forall g ((τ \land [g/ f] τ) \to f = g)$
50	49	adantr	$⊢ (R FrSe A \land \exists f τ) \to \forall f \forall g ((τ \land [g/ f] τ) \to f = g)$
51		nfv	$⊢ Ⅎ g τ$
52	51	eu2	$⊢ \exists! f τ \leftrightarrow (\exists f τ \land \forall f \forall g ((τ \land [g/ f] τ) \to f = g))$
53	5 50 52	sylanbrc	$⊢ (R FrSe A \land \exists f τ) \to \exists! f τ$

Metamath Proof Explorer

Theorem bnj1321

Proof