bnj1450

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

Proof

Step	Hyp	Ref	Expression
1		bnj1450.1	$⊢ B = \{d \| (d \subseteq A \land \forall x \in d pred (x, A, R) \subseteq d)\}$
2		bnj1450.2	$⊢ Y = ⟨x, {f ↾}_{pred (x, A, R)}⟩$
3		bnj1450.3	$⊢ C = \{f \| \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))\}$
4		bnj1450.4	$⊢ τ \leftrightarrow (f \in C \land dom f = \{x\} \cup trCl (x, A, R))$
5		bnj1450.5	$⊢ D = \{x \in A \| \neg \exists f τ\}$
6		bnj1450.6	$⊢ ψ \leftrightarrow (R FrSe A \land D \neq \emptyset)$
7		bnj1450.7	$⊢ χ \leftrightarrow (ψ \land x \in D \land \forall y \in D \neg y R x)$
8		bnj1450.8	Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for \|- ( ta' <-> [. y / x ]. ta ) with typecode \|-
9		bnj1450.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		bnj1450.10	$⊢ P = ⋃ H$
11		bnj1450.11	$⊢ Z = ⟨x, {P ↾}_{pred (x, A, R)}⟩$
12		bnj1450.12	$⊢ Q = P \cup \{⟨x, G (Z)⟩\}$
13		bnj1450.13	$⊢ W = ⟨z, {Q ↾}_{pred (z, A, R)}⟩$
14		bnj1450.14	$⊢ E = \{x\} \cup trCl (x, A, R)$
15		bnj1450.15	$⊢ χ \to P Fn trCl (x, A, R)$
16		bnj1450.16	$⊢ χ \to Q Fn (\{x\} \cup trCl (x, A, R))$
17		bnj1450.17	$⊢ θ \leftrightarrow (χ \land z \in E)$
18		bnj1450.18	$⊢ η \leftrightarrow (θ \land z \in \{x\})$
19		bnj1450.19	$⊢ ζ \leftrightarrow (θ \land z \in trCl (x, A, R))$
20		bnj1450.20	$⊢ ρ \leftrightarrow (ζ \land f \in H \land z \in dom f)$
21		bnj1450.21	$⊢ σ \leftrightarrow (ρ \land y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R))$
22		bnj1450.22	$⊢ φ \leftrightarrow (σ \land d \in B \land f Fn d \land \forall x \in d f (x) = G (Y))$
23		bnj1450.23	$⊢ X = ⟨z, {f ↾}_{pred (z, A, R)}⟩$
24	19	simprbi	$⊢ ζ \to z \in trCl (x, A, R)$
25	15	fndmd	$⊢ χ \to dom P = trCl (x, A, R)$
26	17 25	bnj832	$⊢ θ \to dom P = trCl (x, A, R)$
27	19 26	bnj832	$⊢ ζ \to dom P = trCl (x, A, R)$
28	24 27	eleqtrrd	$⊢ ζ \to z \in dom P$
29	10	dmeqi	$⊢ dom P = dom ⋃ H$
30	28 29	eleqtrdi	$⊢ ζ \to z \in dom ⋃ H$
31	9	bnj1317	$⊢ w \in H \to \forall f w \in H$
32	31	bnj1400	$⊢ dom ⋃ H = ⋃_{f \in H} dom f$
33	30 32	eleqtrdi	$⊢ ζ \to z \in ⋃_{f \in H} dom f$
34	33	bnj1405	$⊢ ζ \to \exists f \in H z \in dom f$
35	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	bnj1449	$⊢ ζ \to \forall f ζ$
36	34 20 35	bnj1521	$⊢ ζ \to \exists f ρ$
37	9	bnj1436	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 \|-
38	20 37	bnj836	Could not format ( rh -> E. y e. _pred ( x , A , R ) ta' ) : No typesetting found for \|- ( rh -> E. y e. _pred ( x , A , R ) ta' ) with typecode \|-
39	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 \|-
40	39	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 \|-
41	38 40	sylib	$⊢ ρ \to \exists y \in pred (x, A, R) (f \in C \land dom f = \{y\} \cup trCl (y, A, R))$
42	41	bnj1196	$⊢ ρ \to \exists y (y \in pred (x, A, R) \land (f \in C \land dom f = \{y\} \cup trCl (y, A, R)))$
43		3anass	$⊢ (y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R)) \leftrightarrow (y \in pred (x, A, R) \land (f \in C \land dom f = \{y\} \cup trCl (y, A, R)))$
44	42 43	bnj1198	$⊢ ρ \to \exists y (y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R))$
45		bnj252	$⊢ (ρ \land y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R)) \leftrightarrow (ρ \land (y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R)))$
46	21 45	bitri	$⊢ σ \leftrightarrow (ρ \land (y \in pred (x, A, R) \land f \in C \land dom f = \{y\} \cup trCl (y, A, R)))$
47	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	bnj1444	$⊢ ρ \to \forall y ρ$
48	44 46 47	bnj1340	$⊢ ρ \to \exists y σ$
49	3	bnj1436	$⊢ f \in C \to \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))$
50	21 49	bnj771	$⊢ σ \to \exists d \in B (f Fn d \land \forall x \in d f (x) = G (Y))$
51	50	bnj1196	$⊢ σ \to \exists d (d \in B \land (f Fn d \land \forall x \in d f (x) = G (Y)))$
52		3anass	$⊢ (d \in B \land f Fn d \land \forall x \in d f (x) = G (Y)) \leftrightarrow (d \in B \land (f Fn d \land \forall x \in d f (x) = G (Y)))$
53	51 52	bnj1198	$⊢ σ \to \exists d (d \in B \land f Fn d \land \forall x \in d f (x) = G (Y))$
54		bnj252	$⊢ (σ \land d \in B \land f Fn d \land \forall x \in d f (x) = G (Y)) \leftrightarrow (σ \land (d \in B \land f Fn d \land \forall x \in d f (x) = G (Y)))$
55	22 54	bitri	$⊢ φ \leftrightarrow (σ \land (d \in B \land f Fn d \land \forall x \in d f (x) = G (Y)))$
56	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	bnj1445	$⊢ σ \to \forall d σ$
57	53 55 56	bnj1340	$⊢ σ \to \exists d φ$
58		fveq2	$⊢ x = z \to f (x) = f (z)$
59		id	$⊢ x = z \to x = z$
60		bnj602	$⊢ x = z \to pred (x, A, R) = pred (z, A, R)$
61	60	reseq2d	$⊢ x = z \to {f ↾}_{pred (x, A, R)} = {f ↾}_{pred (z, A, R)}$
62	59 61	opeq12d	$⊢ x = z \to ⟨x, {f ↾}_{pred (x, A, R)}⟩ = ⟨z, {f ↾}_{pred (z, A, R)}⟩$
63	62 2 23	3eqtr4g	$⊢ x = z \to Y = X$
64	63	fveq2d	$⊢ x = z \to G (Y) = G (X)$
65	58 64	eqeq12d	$⊢ x = z \to (f (x) = G (Y) \leftrightarrow f (z) = G (X))$
66	22	bnj1254	$⊢ φ \to \forall x \in d f (x) = G (Y)$
67	20	simp3bi	$⊢ ρ \to z \in dom f$
68	21 67	bnj769	$⊢ σ \to z \in dom f$
69	22 68	bnj769	$⊢ φ \to z \in dom f$
70		fndm	$⊢ f Fn d \to dom f = d$
71	22 70	bnj771	$⊢ φ \to dom f = d$
72	69 71	eleqtrd	$⊢ φ \to z \in d$
73	65 66 72	rspcdva	$⊢ φ \to f (z) = G (X)$
74	16	fnfund	$⊢ χ \to Fun Q$
75	17 74	bnj832	$⊢ θ \to Fun Q$
76	19 75	bnj832	$⊢ ζ \to Fun Q$
77	20 76	bnj835	$⊢ ρ \to Fun Q$
78	21 77	bnj769	$⊢ σ \to Fun Q$
79	22 78	bnj769	$⊢ φ \to Fun Q$
80	20	simp2bi	$⊢ ρ \to f \in H$
81	21 80	bnj769	$⊢ σ \to f \in H$
82	22 81	bnj769	$⊢ φ \to f \in H$
83		elssuni	$⊢ f \in H \to f \subseteq ⋃ H$
84	83 10	sseqtrrdi	$⊢ f \in H \to f \subseteq P$
85		ssun3	$⊢ f \subseteq P \to f \subseteq P \cup \{⟨x, G (Z)⟩\}$
86	85 12	sseqtrrdi	$⊢ f \subseteq P \to f \subseteq Q$
87	82 84 86	3syl	$⊢ φ \to f \subseteq Q$
88	79 87 69	bnj1502	$⊢ φ \to Q (z) = f (z)$
89	60	sseq1d	$⊢ x = z \to (pred (x, A, R) \subseteq d \leftrightarrow pred (z, A, R) \subseteq d)$
90	1	bnj1517	$⊢ d \in B \to \forall x \in d pred (x, A, R) \subseteq d$
91	22 90	bnj770	$⊢ φ \to \forall x \in d pred (x, A, R) \subseteq d$
92	89 91 72	rspcdva	$⊢ φ \to pred (z, A, R) \subseteq d$
93	92 71	sseqtrrd	$⊢ φ \to pred (z, A, R) \subseteq dom f$
94	79 87 93	bnj1503	$⊢ φ \to {Q ↾}_{pred (z, A, R)} = {f ↾}_{pred (z, A, R)}$
95	94	opeq2d	$⊢ φ \to ⟨z, {Q ↾}_{pred (z, A, R)}⟩ = ⟨z, {f ↾}_{pred (z, A, R)}⟩$
96	95 13 23	3eqtr4g	$⊢ φ \to W = X$
97	96	fveq2d	$⊢ φ \to G (W) = G (X)$
98	73 88 97	3eqtr4d	$⊢ φ \to Q (z) = G (W)$
99	57 98	bnj593	$⊢ σ \to \exists d Q (z) = G (W)$
100	1 2 3 4 5 6 7 8 9 10 11 12 13	bnj1446	$⊢ Q (z) = G (W) \to \forall d Q (z) = G (W)$
101	99 100	bnj1397	$⊢ σ \to Q (z) = G (W)$
102	48 101	bnj593	$⊢ ρ \to \exists y Q (z) = G (W)$
103	1 2 3 4 5 6 7 8 9 10 11 12 13	bnj1447	$⊢ Q (z) = G (W) \to \forall y Q (z) = G (W)$
104	102 103	bnj1397	$⊢ ρ \to Q (z) = G (W)$
105	36 104	bnj593	$⊢ ζ \to \exists f Q (z) = G (W)$
106	1 2 3 4 5 6 7 8 9 10 11 12 13	bnj1448	$⊢ Q (z) = G (W) \to \forall f Q (z) = G (W)$
107	105 106	bnj1397	$⊢ ζ \to Q (z) = G (W)$

Metamath Proof Explorer

Theorem bnj1450

Proof