bnj1498

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	bnj1498.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1498.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1498.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1498.4	$⊢ F = ⋃ C$
Assertion	bnj1498	$⊢ R FrSe A \to dom F = A$

Proof

Step	Hyp	Ref	Expression
1		bnj1498.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1498.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1498.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1498.4	$⊢ F = ⋃ C$
5		eliun	$⊢ z \in ⋃_{f \in C} dom f \leftrightarrow \exists f \in C z \in dom f$
6	3	bnj1436	$⊢ f \in C \to \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))$
7	6	bnj1299	$⊢ f \in C \to \exists d \in B f Fn d$
8		fndm	$⊢ f Fn d \to dom f = d$
9	7 8	bnj31	$⊢ f \in C \to \exists d \in B dom f = d$
10	9	bnj1196	$⊢ f \in C \to \exists d (d \in B \land dom f = d)$
11	1	bnj1436	$⊢ d \in B \to (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)$
12	11	simpld	$⊢ d \in B \to d \subseteq A$
13	12	anim1i	$⊢ (d \in B \land dom f = d) \to (d \subseteq A \land dom f = d)$
14	10 13	bnj593	$⊢ f \in C \to \exists d (d \subseteq A \land dom f = d)$
15		sseq1	$⊢ dom f = d \to (dom f \subseteq A \leftrightarrow d \subseteq A)$
16	15	biimparc	$⊢ (d \subseteq A \land dom f = d) \to dom f \subseteq A$
17	14 16	bnj593	$⊢ f \in C \to \exists d dom f \subseteq A$
18	17	bnj937	$⊢ f \in C \to dom f \subseteq A$
19	18	sselda	$⊢ (f \in C \land z \in dom f) \to z \in A$
20	19	rexlimiva	$⊢ \exists f \in C z \in dom f \to z \in A$
21	5 20	sylbi	$⊢ z \in ⋃_{f \in C} dom f \to z \in A$
22	3	bnj1317	$⊢ w \in C \to \forall f w \in C$
23	22	bnj1400	$⊢ dom ⋃ C = ⋃_{f \in C} dom f$
24	21 23	eleq2s	$⊢ z \in dom ⋃ C \to z \in A$
25	4	dmeqi	$⊢ dom F = dom ⋃ C$
26	24 25	eleq2s	$⊢ z \in dom F \to z \in A$
27	26	ssriv	$⊢ dom F \subseteq A$
28	27	a1i	$⊢ R FrSe A \to dom F \subseteq A$
29	1 2 3	bnj1493	$⊢ R FrSe A \to \forall x \in A \exists f \in C dom f = \{x\} \cup trCl (x, A, R)$
30		vsnid	$⊢ x \in \{x\}$
31		elun1	$⊢ x \in \{x\} \to x \in (\{x\} \cup trCl (x, A, R))$
32	30 31	ax-mp	$⊢ x \in (\{x\} \cup trCl (x, A, R))$
33		eleq2	$⊢ dom f = \{x\} \cup trCl (x, A, R) \to (x \in dom f \leftrightarrow x \in (\{x\} \cup trCl (x, A, R)))$
34	32 33	mpbiri	$⊢ dom f = \{x\} \cup trCl (x, A, R) \to x \in dom f$
35	34	reximi	$⊢ \exists f \in C dom f = \{x\} \cup trCl (x, A, R) \to \exists f \in C x \in dom f$
36	35	ralimi	$⊢ \forall x \in A \exists f \in C dom f = \{x\} \cup trCl (x, A, R) \to \forall x \in A \exists f \in C x \in dom f$
37	29 36	syl	$⊢ R FrSe A \to \forall x \in A \exists f \in C x \in dom f$
38		eliun	$⊢ x \in ⋃_{f \in C} dom f \leftrightarrow \exists f \in C x \in dom f$
39	38	ralbii	$⊢ \forall x \in A x \in ⋃_{f \in C} dom f \leftrightarrow \forall x \in A \exists f \in C x \in dom f$
40	37 39	sylibr	$⊢ R FrSe A \to \forall x \in A x \in ⋃_{f \in C} dom f$
41		nfcv	$⊢ \underline{Ⅎ} x A$
42	1	bnj1309	$⊢ t \in B \to \forall x t \in B$
43	3 42	bnj1307	$⊢ t \in C \to \forall x t \in C$
44	43	nfcii	$⊢ \underline{Ⅎ} x C$
45		nfcv	$⊢ \underline{Ⅎ} x dom f$
46	44 45	nfiun	$⊢ \underline{Ⅎ} x ⋃_{f \in C} dom f$
47	41 46	dfss3f	$⊢ A \subseteq ⋃_{f \in C} dom f \leftrightarrow \forall x \in A x \in ⋃_{f \in C} dom f$
48	40 47	sylibr	$⊢ R FrSe A \to A \subseteq ⋃_{f \in C} dom f$
49	48 23	sseqtrrdi	$⊢ R FrSe A \to A \subseteq dom ⋃ C$
50	49 25	sseqtrrdi	$⊢ R FrSe A \to A \subseteq dom F$
51	28 50	eqssd	$⊢ R FrSe A \to dom F = A$

Metamath Proof Explorer

Theorem bnj1498

Proof