bnj1398

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	bnj1398.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
	bnj1398.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
	bnj1398.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
	bnj1398.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
	bnj1398.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
	bnj1398.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
	bnj1398.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
	bnj1398.8	No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
	bnj1398.9	No typesetting found for \|- H = { f \| E. y e. _pred ( x , A , R ) ta' } with typecode \|-
	bnj1398.10	$⊢ P = ⋃ H$
	bnj1398.11	$⊢ θ \leftrightarrow (χ \land z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)))$
	bnj1398.12	$⊢ η \leftrightarrow (θ \land y \in pred (x, A, R) \land z \in (\{y\} \cup trCl (y, A, R)))$
Assertion	bnj1398	$⊢ χ \to ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) = dom P$

Proof

Step	Hyp	Ref	Expression
1		bnj1398.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1398.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1398.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1398.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		bnj1398.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
6		bnj1398.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
7		bnj1398.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
8		bnj1398.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
9		bnj1398.9	Could not format H = { f \| E. y e. _pred ( x , A , R ) ta' } : No typesetting found for \|- H = { f \| E. y e. _pred ( x , A , R ) ta' } with typecode \|-
10		bnj1398.10	$⊢ P = ⋃ H$
11		bnj1398.11	$⊢ θ \leftrightarrow (χ \land z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)))$
12		bnj1398.12	$⊢ η \leftrightarrow (θ \land y \in pred (x, A, R) \land z \in (\{y\} \cup trCl (y, A, R)))$
13		df-iun	$⊢ ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) = \{z \| \exists y \in pred (x, A, R) z \in (\{y\} \cup trCl (y, A, R))\}$
14	13	bnj1436	$⊢ z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) \to \exists y \in pred (x, A, R) z \in (\{y\} \cup trCl (y, A, R))$
15	11 14	simplbiim	$⊢ θ \to \exists y \in pred (x, A, R) z \in (\{y\} \cup trCl (y, A, R))$
16		nfv	$⊢ Ⅎ y ψ$
17		nfv	$⊢ Ⅎ y x \in D$
18		nfra1	$⊢ Ⅎ y \forall y \in D \neg y R x$
19	16 17 18	nf3an	$⊢ Ⅎ y (ψ \land x \in D \land \forall y \in D \neg y R x)$
20	7 19	nfxfr	$⊢ Ⅎ y χ$
21		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))$
22	21	nfcri	$⊢ Ⅎ y z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))$
23	20 22	nfan	$⊢ Ⅎ y (χ \land z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)))$
24	11 23	nfxfr	$⊢ Ⅎ y θ$
25	24	nf5ri	$⊢ θ \to \forall y θ$
26	15 12 25	bnj1521	$⊢ θ \to \exists y η$
27		nfv	$⊢ Ⅎ f R FrSe A$
28		nfe1	$⊢ Ⅎ f \exists f τ$
29	28	nfn	$⊢ Ⅎ f \neg \exists f τ$
30		nfcv	$⊢ \underline{Ⅎ} f A$
31	29 30	nfrabw	$⊢ \underline{Ⅎ} f \{x \in A \| \neg \exists f τ\}$
32	5 31	nfcxfr	$⊢ \underline{Ⅎ} f D$
33		nfcv	$⊢ \underline{Ⅎ} f \emptyset$
34	32 33	nfne	$⊢ Ⅎ f D \neq \emptyset$
35	27 34	nfan	$⊢ Ⅎ f (R FrSe A \land D \neq \emptyset)$
36	6 35	nfxfr	$⊢ Ⅎ f ψ$
37	32	nfcri	$⊢ Ⅎ f x \in D$
38		nfv	$⊢ Ⅎ f \neg y R x$
39	32 38	nfralw	$⊢ Ⅎ f \forall y \in D \neg y R x$
40	36 37 39	nf3an	$⊢ Ⅎ f (ψ \land x \in D \land \forall y \in D \neg y R x)$
41	7 40	nfxfr	$⊢ Ⅎ f χ$
42		nfv	$⊢ Ⅎ f z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))$
43	41 42	nfan	$⊢ Ⅎ f (χ \land z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)))$
44	11 43	nfxfr	$⊢ Ⅎ f θ$
45		nfv	$⊢ Ⅎ f y \in pred (x, A, R)$
46		nfv	$⊢ Ⅎ f z \in (\{y\} \cup trCl (y, A, R))$
47	44 45 46	nf3an	$⊢ Ⅎ f (θ \land y \in pred (x, A, R) \land z \in (\{y\} \cup trCl (y, A, R)))$
48	12 47	nfxfr	$⊢ Ⅎ f η$
49	48	nf5ri	$⊢ η \to \forall f η$
50	11	simplbi	$⊢ θ \to χ$
51	12 50	bnj835	$⊢ η \to χ$
52	12	simp2bi	$⊢ η \to y \in pred (x, A, R)$
53	1 2 3 4 5 6 7 8	bnj1388	Could not format ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) : No typesetting found for \|- ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) with typecode \|-
54		rsp	Could not format ( A. y e. _pred ( x , A , R ) E. f ta' -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) : No typesetting found for \|- ( A. y e. _pred ( x , A , R ) E. f ta' -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) with typecode \|-
55	53 54	syl	Could not format ( ch -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) : No typesetting found for \|- ( ch -> ( y e. _pred ( x , A , R ) -> E. f ta' ) ) with typecode \|-
56	51 52 55	sylc	Could not format ( et -> E. f ta' ) : No typesetting found for \|- ( et -> E. f ta' ) with typecode \|-
57	49 56	bnj596	Could not format ( et -> E. f ( et /\ ta' ) ) : No typesetting found for \|- ( et -> E. f ( et /\ ta' ) ) with typecode \|-
58	1 2 3 4 8	bnj1373	Could not format ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for \|- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode \|-
59	58	simplbi	Could not format ( ta' -> f e. C ) : No typesetting found for \|- ( ta' -> f e. C ) with typecode \|-
60	59	adantl	Could not format ( ( et /\ ta' ) -> f e. C ) : No typesetting found for \|- ( ( et /\ ta' ) -> f e. C ) with typecode \|-
61	58	simprbi	Could not format ( ta' -> dom f = ( { y } u. _trCl ( y , A , R ) ) ) : No typesetting found for \|- ( ta' -> dom f = ( { y } u. _trCl ( y , A , R ) ) ) with typecode \|-
62		rspe	$⊢ (y \in pred (x, A, R) \land dom f = \{y\} \cup trCl (y, A, R)) \to \exists y \in pred (x, A, R) dom f = \{y\} \cup trCl (y, A, R)$
63	52 61 62	syl2an	Could not format ( ( et /\ ta' ) -> E. y e. _pred ( x , A , R ) dom f = ( { y } u. _trCl ( y , A , R ) ) ) : No typesetting found for \|- ( ( et /\ ta' ) -> E. y e. _pred ( x , A , R ) dom f = ( { y } u. _trCl ( y , A , R ) ) ) with typecode \|-
64	9	abeq2i	Could not format ( f e. H <-> E. y e. _pred ( x , A , R ) ta' ) : No typesetting found for \|- ( f e. H <-> E. y e. _pred ( x , A , R ) ta' ) with typecode \|-
65	58	rexbii	Could not format ( E. y e. _pred ( x , A , R ) ta' <-> E. y e. _pred ( x , A , R ) ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for \|- ( E. y e. _pred ( x , A , R ) ta' <-> E. y e. _pred ( x , A , R ) ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode \|-
66		r19.42v	$⊢ \exists y \in pred (x, A, R) (f \in C \land dom f = \{y\} \cup trCl (y, A, R)) \leftrightarrow (f \in C \land \exists y \in pred (x, A, R) dom f = \{y\} \cup trCl (y, A, R))$
67	64 65 66	3bitri	$⊢ f \in H \leftrightarrow (f \in C \land \exists y \in pred (x, A, R) dom f = \{y\} \cup trCl (y, A, R))$
68	60 63 67	sylanbrc	Could not format ( ( et /\ ta' ) -> f e. H ) : No typesetting found for \|- ( ( et /\ ta' ) -> f e. H ) with typecode \|-
69	12	simp3bi	$⊢ η \to z \in (\{y\} \cup trCl (y, A, R))$
70	69	adantr	Could not format ( ( et /\ ta' ) -> z e. ( { y } u. _trCl ( y , A , R ) ) ) : No typesetting found for \|- ( ( et /\ ta' ) -> z e. ( { y } u. _trCl ( y , A , R ) ) ) with typecode \|-
71	61	adantl	Could not format ( ( et /\ ta' ) -> dom f = ( { y } u. _trCl ( y , A , R ) ) ) : No typesetting found for \|- ( ( et /\ ta' ) -> dom f = ( { y } u. _trCl ( y , A , R ) ) ) with typecode \|-
72	70 71	eleqtrrd	Could not format ( ( et /\ ta' ) -> z e. dom f ) : No typesetting found for \|- ( ( et /\ ta' ) -> z e. dom f ) with typecode \|-
73	68 72	jca	Could not format ( ( et /\ ta' ) -> ( f e. H /\ z e. dom f ) ) : No typesetting found for \|- ( ( et /\ ta' ) -> ( f e. H /\ z e. dom f ) ) with typecode \|-
74	57 73	bnj593	$⊢ η \to \exists f (f \in H \land z \in dom f)$
75		df-rex	$⊢ \exists f \in H z \in dom f \leftrightarrow \exists f (f \in H \land z \in dom f)$
76	74 75	sylibr	$⊢ η \to \exists f \in H z \in dom f$
77	10	dmeqi	$⊢ dom P = dom ⋃ H$
78	9	bnj1317	$⊢ w \in H \to \forall f w \in H$
79	78	bnj1400	$⊢ dom ⋃ H = ⋃_{f \in H} dom f$
80	77 79	eqtri	$⊢ dom P = ⋃_{f \in H} dom f$
81	80	eleq2i	$⊢ z \in dom P \leftrightarrow z \in ⋃_{f \in H} dom f$
82		eliun	$⊢ z \in ⋃_{f \in H} dom f \leftrightarrow \exists f \in H z \in dom f$
83	81 82	bitri	$⊢ z \in dom P \leftrightarrow \exists f \in H z \in dom f$
84	76 83	sylibr	$⊢ η \to z \in dom P$
85	26 84	bnj593	$⊢ θ \to \exists y z \in dom P$
86		nfre1	Could not format F/ y E. y e. _pred ( x , A , R ) ta' : No typesetting found for \|- F/ y E. y e. _pred ( x , A , R ) ta' with typecode \|-
87	86	nfab	Could not format F/_ y { f \| E. y e. _pred ( x , A , R ) ta' } : No typesetting found for \|- F/_ y { f \| E. y e. _pred ( x , A , R ) ta' } with typecode \|-
88	9 87	nfcxfr	$⊢ \underline{Ⅎ} y H$
89	88	nfuni	$⊢ \underline{Ⅎ} y ⋃ H$
90	10 89	nfcxfr	$⊢ \underline{Ⅎ} y P$
91	90	nfdm	$⊢ \underline{Ⅎ} y dom P$
92	91	nfcrii	$⊢ z \in dom P \to \forall y z \in dom P$
93	85 92	bnj1397	$⊢ θ \to z \in dom P$
94	11 93	sylbir	$⊢ (χ \land z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))) \to z \in dom P$
95	94	ex	$⊢ χ \to (z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) \to z \in dom P)$
96	95	ssrdv	$⊢ χ \to ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) \subseteq dom P$
97		simpr	$⊢ (f \in H \land z \in dom f) \to z \in dom f$
98	67	simprbi	$⊢ f \in H \to \exists y \in pred (x, A, R) dom f = \{y\} \cup trCl (y, A, R)$
99	98	adantr	$⊢ (f \in H \land z \in dom f) \to \exists y \in pred (x, A, R) dom f = \{y\} \cup trCl (y, A, R)$
100		r19.42v	$⊢ \exists y \in pred (x, A, R) (z \in dom f \land dom f = \{y\} \cup trCl (y, A, R)) \leftrightarrow (z \in dom f \land \exists y \in pred (x, A, R) dom f = \{y\} \cup trCl (y, A, R))$
101		eleq2	$⊢ dom f = \{y\} \cup trCl (y, A, R) \to (z \in dom f \leftrightarrow z \in (\{y\} \cup trCl (y, A, R)))$
102	101	biimpac	$⊢ (z \in dom f \land dom f = \{y\} \cup trCl (y, A, R)) \to z \in (\{y\} \cup trCl (y, A, R))$
103	102	reximi	$⊢ \exists y \in pred (x, A, R) (z \in dom f \land dom f = \{y\} \cup trCl (y, A, R)) \to \exists y \in pred (x, A, R) z \in (\{y\} \cup trCl (y, A, R))$
104	100 103	sylbir	$⊢ (z \in dom f \land \exists y \in pred (x, A, R) dom f = \{y\} \cup trCl (y, A, R)) \to \exists y \in pred (x, A, R) z \in (\{y\} \cup trCl (y, A, R))$
105	97 99 104	syl2anc	$⊢ (f \in H \land z \in dom f) \to \exists y \in pred (x, A, R) z \in (\{y\} \cup trCl (y, A, R))$
106	105	rexlimiva	$⊢ \exists f \in H z \in dom f \to \exists y \in pred (x, A, R) z \in (\{y\} \cup trCl (y, A, R))$
107		eliun	$⊢ z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) \leftrightarrow \exists y \in pred (x, A, R) z \in (\{y\} \cup trCl (y, A, R))$
108	106 83 107	3imtr4i	$⊢ z \in dom P \to z \in ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))$
109	108	ssriv	$⊢ dom P \subseteq ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))$
110	109	a1i	$⊢ χ \to dom P \subseteq ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R))$
111	96 110	eqssd	$⊢ χ \to ⋃_{y \in pred (x, A, R)} (\{y\} \cup trCl (y, A, R)) = dom P$

Metamath Proof Explorer

Theorem bnj1398

Proof