bnj1489

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

Proof

Step	Hyp	Ref	Expression
1		bnj1489.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1489.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1489.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1489.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		bnj1489.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
6		bnj1489.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
7		bnj1489.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
8		bnj1489.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
9		bnj1489.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		bnj1489.10	$⊢ P = ⋃ H$
11		bnj1489.11	$⊢ Z = ⟨x, {P ↾}_{pred (x, A, R)}⟩$
12		bnj1489.12	$⊢ Q = P \cup \{⟨x, G (Z)⟩\}$
13		bnj1364	$⊢ R FrSe A \to R Se A$
14		df-bnj13	$⊢ R Se A \leftrightarrow \forall x \in A pred (x, A, R) \in V$
15	13 14	sylib	$⊢ R FrSe A \to \forall x \in A pred (x, A, R) \in V$
16	6 15	bnj832	$⊢ ψ \to \forall x \in A pred (x, A, R) \in V$
17	7 16	bnj835	$⊢ χ \to \forall x \in A pred (x, A, R) \in V$
18	5 7	bnj1212	$⊢ χ \to x \in A$
19	17 18	bnj1294	$⊢ χ \to pred (x, A, R) \in V$
20		nfv	$⊢ Ⅎ y ψ$
21		nfv	$⊢ Ⅎ y x \in D$
22		nfra1	$⊢ Ⅎ y \forall y \in D \neg y R x$
23	20 21 22	nf3an	$⊢ Ⅎ y (ψ \land x \in D \land \forall y \in D \neg y R x)$
24	7 23	nfxfr	$⊢ Ⅎ y χ$
25	6	simplbi	$⊢ ψ \to R FrSe A$
26	7 25	bnj835	$⊢ χ \to R FrSe A$
27	26	adantr	$⊢ (χ \land y \in pred (x, A, R)) \to R FrSe A$
28	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 \|-
29	28	r19.21bi	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 \|-
30		nfv	$⊢ Ⅎ x R FrSe A$
31		nfsbc1v	$⊢ Ⅎ x \underset{˙}{[} y / x \underset{˙}{]} τ$
32	8 31	nfxfr	Could not format F/ x ta' : No typesetting found for \|- F/ x ta' with typecode \|-
33	32	nfex	Could not format F/ x E. f ta' : No typesetting found for \|- F/ x E. f ta' with typecode \|-
34	30 33	nfan	Could not format F/ x ( R _FrSe A /\ E. f ta' ) : No typesetting found for \|- F/ x ( R _FrSe A /\ E. f ta' ) with typecode \|-
35	32	nfeuw	Could not format F/ x E! f ta' : No typesetting found for \|- F/ x E! f ta' with typecode \|-
36	34 35	nfim	Could not format F/ x ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) : No typesetting found for \|- F/ x ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) with typecode \|-
37		sneq	$⊢ x = y \to \{x\} = \{y\}$
38		bnj1318	$⊢ x = y \to trCl (x, A, R) = trCl (y, A, R)$
39	37 38	uneq12d	$⊢ x = y \to \{x\} \cup trCl (x, A, R) = \{y\} \cup trCl (y, A, R)$
40	39	eqeq2d	$⊢ x = y \to (dom f = \{x\} \cup trCl (x, A, R) \leftrightarrow dom f = \{y\} \cup trCl (y, A, R))$
41	40	anbi2d	$⊢ x = y \to ((f \in C \land dom f = \{x\} \cup trCl (x, A, R)) \leftrightarrow (f \in C \land dom f = \{y\} \cup trCl (y, A, R)))$
42	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 \|-
43	41 42	bitr4di	Could not format ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ta' ) ) : No typesetting found for \|- ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ta' ) ) with typecode \|-
44	43	exbidv	Could not format ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E. f ta' ) ) : No typesetting found for \|- ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E. f ta' ) ) with typecode \|-
45	44	anbi2d	Could not format ( x = y -> ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( R _FrSe A /\ E. f ta' ) ) ) : No typesetting found for \|- ( x = y -> ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( R _FrSe A /\ E. f ta' ) ) ) with typecode \|-
46	43	eubidv	Could not format ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E! f ta' ) ) : No typesetting found for \|- ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E! f ta' ) ) with typecode \|-
47	45 46	imbi12d	Could not format ( x = y -> ( ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) ) ) : No typesetting found for \|- ( x = y -> ( ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) ) ) with typecode \|-
48		biid	$⊢ (f \in C \land dom f = \{x\} \cup trCl (x, A, R)) \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
49	1 2 3 48	bnj1321	$⊢ (R FrSe A \land \exists f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))) \to \exists! f (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
50	36 47 49	chvarfv	Could not format ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) : No typesetting found for \|- ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) with typecode \|-
51	27 29 50	syl2anc	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 \|-
52	51	ex	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 \|-
53	24 52	ralrimi	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	9	a1i	Could not format ( ch -> H = { f \| E. y e. _pred ( x , A , R ) ta' } ) : No typesetting found for \|- ( ch -> H = { f \| E. y e. _pred ( x , A , R ) ta' } ) with typecode \|-
55		biid	Could not format ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f \| E. y e. _pred ( x , A , R ) ta' } ) <-> ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f \| E. y e. _pred ( x , A , R ) ta' } ) ) : No typesetting found for \|- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f \| E. y e. _pred ( x , A , R ) ta' } ) <-> ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f \| E. y e. _pred ( x , A , R ) ta' } ) ) with typecode \|-
56	55	bnj1366	Could not format ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f \| E. y e. _pred ( x , A , R ) ta' } ) -> H e. _V ) : No typesetting found for \|- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f \| E. y e. _pred ( x , A , R ) ta' } ) -> H e. _V ) with typecode \|-
57	19 53 54 56	syl3anc	$⊢ χ \to H \in V$
58	57	uniexd	$⊢ χ \to ⋃ H \in V$
59	10 58	eqeltrid	$⊢ χ \to P \in V$
60		snex	$⊢ \{⟨x, G (Z)⟩\} \in V$
61	60	a1i	$⊢ χ \to \{⟨x, G (Z)⟩\} \in V$
62	59 61	bnj1149	$⊢ χ \to P \cup \{⟨x, G (Z)⟩\} \in V$
63	12 62	eqeltrid	$⊢ χ \to Q \in V$

Metamath Proof Explorer

Theorem bnj1489

Proof