Theorem bnj1385

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1385.1	$$⊢\phi \leftrightarrow \forall f\in A\mathrm{Fun}f$$
	bnj1385.2	$$⊢D=\mathrm{dom}f\cap \mathrm{dom}g$$
	bnj1385.3	$$⊢\psi \leftrightarrow \left(\phi \wedge \forall f\in A\forall g\in A{f\upharpoonright }_D={g\upharpoonright }_D\right)$$
	bnj1385.4	$$⊢x\in A\to \forall fx\in A$$
	bnj1385.5	No typesetting found for |- ( ph' <-> A. h e. A Fun h ) with typecode |-
	bnj1385.6	$$⊢E=\mathrm{dom}h\cap \mathrm{dom}g$$
	bnj1385.7	No typesetting found for |- ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) with typecode |-
Assertion	bnj1385	$$⊢\psi \to \mathrm{Fun}\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		bnj1385.1	$$⊢\phi \leftrightarrow \forall f\in A\mathrm{Fun}f$$
2		bnj1385.2	$$⊢D=\mathrm{dom}f\cap \mathrm{dom}g$$
3		bnj1385.3	$$⊢\psi \leftrightarrow \left(\phi \wedge \forall f\in A\forall g\in A{f\upharpoonright }_D={g\upharpoonright }_D\right)$$
4		bnj1385.4	$$⊢x\in A\to \forall fx\in A$$
5		bnj1385.5	Could not format ( ph' <-> A. h e. A Fun h ) : No typesetting found for |- ( ph' <-> A. h e. A Fun h ) with typecode |-
6		bnj1385.6	$$⊢E=\mathrm{dom}h\cap \mathrm{dom}g$$
7		bnj1385.7	Could not format ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) : No typesetting found for |- ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) with typecode |-
8		nfv	$$⊢Ⅎh\left(f\in A\to \mathrm{Fun}f\right)$$
9	4	nfcii	$$⊢\underset{\_}{Ⅎ}fA$$
10	9	nfcri	$$⊢Ⅎfh\in A$$
11		nfv	$$⊢Ⅎf\mathrm{Fun}h$$
12	10 11	nfim	$$⊢Ⅎf\left(h\in A\to \mathrm{Fun}h\right)$$
13		eleq1w	$$⊢f=h\to \left(f\in A\leftrightarrow h\in A\right)$$
14		funeq	$$⊢f=h\to \left(\mathrm{Fun}f\leftrightarrow \mathrm{Fun}h\right)$$
15	13 14	imbi12d	$$⊢f=h\to \left(\left(f\in A\to \mathrm{Fun}f\right)\leftrightarrow \left(h\in A\to \mathrm{Fun}h\right)\right)$$
16	8 12 15	cbvalv1	$$⊢\forall f\left(f\in A\to \mathrm{Fun}f\right)\leftrightarrow \forall h\left(h\in A\to \mathrm{Fun}h\right)$$
17		df-ral	$$⊢\forall f\in A\mathrm{Fun}f\leftrightarrow \forall f\left(f\in A\to \mathrm{Fun}f\right)$$
18		df-ral	$$⊢\forall h\in A\mathrm{Fun}h\leftrightarrow \forall h\left(h\in A\to \mathrm{Fun}h\right)$$
19	16 17 18	3bitr4i	$$⊢\forall f\in A\mathrm{Fun}f\leftrightarrow \forall h\in A\mathrm{Fun}h$$
20	19 1 5	3bitr4i	Could not format ( ph <-> ph' ) : No typesetting found for |- ( ph <-> ph' ) with typecode |-
21		nfv	$$⊢Ⅎh\left(f\in A\to \forall g\in A{f\upharpoonright }_D={g\upharpoonright }_D\right)$$
22		nfv	$$⊢Ⅎf{h\upharpoonright }_E={g\upharpoonright }_E$$
23	9 22	nfralw	$$⊢Ⅎf\forall g\in A{h\upharpoonright }_E={g\upharpoonright }_E$$
24	10 23	nfim	$$⊢Ⅎf\left(h\in A\to \forall g\in A{h\upharpoonright }_E={g\upharpoonright }_E\right)$$
25		dmeq	$$⊢f=h\to \mathrm{dom}f=\mathrm{dom}h$$
26	25	ineq1d	$$⊢f=h\to \mathrm{dom}f\cap \mathrm{dom}g=\mathrm{dom}h\cap \mathrm{dom}g$$
27	26 2 6	3eqtr4g	$$⊢f=h\to D=E$$
28	27	reseq2d	$$⊢f=h\to {f\upharpoonright }_D={f\upharpoonright }_E$$
29		reseq1	$$⊢f=h\to {f\upharpoonright }_E={h\upharpoonright }_E$$
30	28 29	eqtrd	$$⊢f=h\to {f\upharpoonright }_D={h\upharpoonright }_E$$
31	27	reseq2d	$$⊢f=h\to {g\upharpoonright }_D={g\upharpoonright }_E$$
32	30 31	eqeq12d	$$⊢f=h\to \left({f\upharpoonright }_D={g\upharpoonright }_D\leftrightarrow {h\upharpoonright }_E={g\upharpoonright }_E\right)$$
33	32	ralbidv	$$⊢f=h\to \left(\forall g\in A{f\upharpoonright }_D={g\upharpoonright }_D\leftrightarrow \forall g\in A{h\upharpoonright }_E={g\upharpoonright }_E\right)$$
34	13 33	imbi12d	$$⊢f=h\to \left(\left(f\in A\to \forall g\in A{f\upharpoonright }_D={g\upharpoonright }_D\right)\leftrightarrow \left(h\in A\to \forall g\in A{h\upharpoonright }_E={g\upharpoonright }_E\right)\right)$$
35	21 24 34	cbvalv1	$$⊢\forall f\left(f\in A\to \forall g\in A{f\upharpoonright }_D={g\upharpoonright }_D\right)\leftrightarrow \forall h\left(h\in A\to \forall g\in A{h\upharpoonright }_E={g\upharpoonright }_E\right)$$
36		df-ral	$$⊢\forall f\in A\forall g\in A{f\upharpoonright }_D={g\upharpoonright }_D\leftrightarrow \forall f\left(f\in A\to \forall g\in A{f\upharpoonright }_D={g\upharpoonright }_D\right)$$
37		df-ral	$$⊢\forall h\in A\forall g\in A{h\upharpoonright }_E={g\upharpoonright }_E\leftrightarrow \forall h\left(h\in A\to \forall g\in A{h\upharpoonright }_E={g\upharpoonright }_E\right)$$
38	35 36 37	3bitr4i	$$⊢\forall f\in A\forall g\in A{f\upharpoonright }_D={g\upharpoonright }_D\leftrightarrow \forall h\in A\forall g\in A{h\upharpoonright }_E={g\upharpoonright }_E$$
39	20 38	anbi12i	Could not format ( ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) : No typesetting found for |- ( ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) ) with typecode |-
40	39 3 7	3bitr4i	Could not format ( ps <-> ps' ) : No typesetting found for |- ( ps <-> ps' ) with typecode |-
41	5 6 7	bnj1383	Could not format ( ps' -> Fun U. A ) : No typesetting found for |- ( ps' -> Fun U. A ) with typecode |-
42	40 41	sylbi	$$⊢\psi \to \mathrm{Fun}\bigcup A$$