bnj1379

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

	Ref	Expression
Hypotheses	bnj1379.1	$⊢ φ \leftrightarrow \forall f \in A Fun f$
	bnj1379.2	$⊢ D = dom f \cap dom g$
	bnj1379.3	$⊢ ψ \leftrightarrow (φ \land \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D})$
	bnj1379.5	$⊢ χ \leftrightarrow (ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A)$
	bnj1379.6	$⊢ θ \leftrightarrow (χ \land f \in A \land ⟨x, y⟩ \in f)$
	bnj1379.7	$⊢ τ \leftrightarrow (θ \land g \in A \land ⟨x, z⟩ \in g)$
Assertion	bnj1379	$⊢ ψ \to Fun ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		bnj1379.1	$⊢ φ \leftrightarrow \forall f \in A Fun f$
2		bnj1379.2	$⊢ D = dom f \cap dom g$
3		bnj1379.3	$⊢ ψ \leftrightarrow (φ \land \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D})$
4		bnj1379.5	$⊢ χ \leftrightarrow (ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A)$
5		bnj1379.6	$⊢ θ \leftrightarrow (χ \land f \in A \land ⟨x, y⟩ \in f)$
6		bnj1379.7	$⊢ τ \leftrightarrow (θ \land g \in A \land ⟨x, z⟩ \in g)$
7	1	bnj1095	$⊢ φ \to \forall f φ$
8	7	nf5i	$⊢ Ⅎ f φ$
9		nfra1	$⊢ Ⅎ f \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D}$
10	8 9	nfan	$⊢ Ⅎ f (φ \land \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D})$
11	3 10	nfxfr	$⊢ Ⅎ f ψ$
12	1	bnj946	$⊢ φ \leftrightarrow \forall f (f \in A \to Fun f)$
13	12	biimpi	$⊢ φ \to \forall f (f \in A \to Fun f)$
14	13	19.21bi	$⊢ φ \to (f \in A \to Fun f)$
15	3 14	bnj832	$⊢ ψ \to (f \in A \to Fun f)$
16		funrel	$⊢ Fun f \to Rel f$
17	15 16	syl6	$⊢ ψ \to (f \in A \to Rel f)$
18	11 17	ralrimi	$⊢ ψ \to \forall f \in A Rel f$
19		reluni	$⊢ Rel ⋃ A \leftrightarrow \forall f \in A Rel f$
20	18 19	sylibr	$⊢ ψ \to Rel ⋃ A$
21		eluni2	$⊢ ⟨x, y⟩ \in ⋃ A \leftrightarrow \exists f \in A ⟨x, y⟩ \in f$
22	21	biimpi	$⊢ ⟨x, y⟩ \in ⋃ A \to \exists f \in A ⟨x, y⟩ \in f$
23	22	bnj1196	$⊢ ⟨x, y⟩ \in ⋃ A \to \exists f (f \in A \land ⟨x, y⟩ \in f)$
24	4 23	bnj836	$⊢ χ \to \exists f (f \in A \land ⟨x, y⟩ \in f)$
25		nfv	$⊢ Ⅎ f ⟨x, y⟩ \in ⋃ A$
26		nfv	$⊢ Ⅎ f ⟨x, z⟩ \in ⋃ A$
27	11 25 26	nf3an	$⊢ Ⅎ f (ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A)$
28	4 27	nfxfr	$⊢ Ⅎ f χ$
29	28	nf5ri	$⊢ χ \to \forall f χ$
30	24 5 29	bnj1345	$⊢ χ \to \exists f θ$
31	4	simp3bi	$⊢ χ \to ⟨x, z⟩ \in ⋃ A$
32	5 31	bnj835	$⊢ θ \to ⟨x, z⟩ \in ⋃ A$
33		eluni2	$⊢ ⟨x, z⟩ \in ⋃ A \leftrightarrow \exists g \in A ⟨x, z⟩ \in g$
34	33	biimpi	$⊢ ⟨x, z⟩ \in ⋃ A \to \exists g \in A ⟨x, z⟩ \in g$
35	34	bnj1196	$⊢ ⟨x, z⟩ \in ⋃ A \to \exists g (g \in A \land ⟨x, z⟩ \in g)$
36	32 35	syl	$⊢ θ \to \exists g (g \in A \land ⟨x, z⟩ \in g)$
37		nfv	$⊢ Ⅎ g φ$
38		nfra2w	$⊢ Ⅎ g \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D}$
39	37 38	nfan	$⊢ Ⅎ g (φ \land \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D})$
40	3 39	nfxfr	$⊢ Ⅎ g ψ$
41		nfv	$⊢ Ⅎ g ⟨x, y⟩ \in ⋃ A$
42		nfv	$⊢ Ⅎ g ⟨x, z⟩ \in ⋃ A$
43	40 41 42	nf3an	$⊢ Ⅎ g (ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A)$
44	4 43	nfxfr	$⊢ Ⅎ g χ$
45		nfv	$⊢ Ⅎ g f \in A$
46		nfv	$⊢ Ⅎ g ⟨x, y⟩ \in f$
47	44 45 46	nf3an	$⊢ Ⅎ g (χ \land f \in A \land ⟨x, y⟩ \in f)$
48	5 47	nfxfr	$⊢ Ⅎ g θ$
49	48	nf5ri	$⊢ θ \to \forall g θ$
50	36 6 49	bnj1345	$⊢ θ \to \exists g τ$
51	3	simprbi	$⊢ ψ \to \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D}$
52	4 51	bnj835	$⊢ χ \to \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D}$
53	5 52	bnj835	$⊢ θ \to \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D}$
54	6 53	bnj835	$⊢ τ \to \forall f \in A \forall g \in A {f ↾}_{D} = {g ↾}_{D}$
55	5 6	bnj1219	$⊢ τ \to f \in A$
56	54 55	bnj1294	$⊢ τ \to \forall g \in A {f ↾}_{D} = {g ↾}_{D}$
57	6	simp2bi	$⊢ τ \to g \in A$
58	56 57	bnj1294	$⊢ τ \to {f ↾}_{D} = {g ↾}_{D}$
59	58	fveq1d	$⊢ τ \to ({f ↾}_{D}) (x) = ({g ↾}_{D}) (x)$
60	5	simp3bi	$⊢ θ \to ⟨x, y⟩ \in f$
61	6 60	bnj835	$⊢ τ \to ⟨x, y⟩ \in f$
62		vex	$⊢ x \in V$
63		vex	$⊢ y \in V$
64	62 63	opeldm	$⊢ ⟨x, y⟩ \in f \to x \in dom f$
65	61 64	syl	$⊢ τ \to x \in dom f$
66		vex	$⊢ z \in V$
67	62 66	opeldm	$⊢ ⟨x, z⟩ \in g \to x \in dom g$
68	6 67	bnj837	$⊢ τ \to x \in dom g$
69	65 68	elind	$⊢ τ \to x \in (dom f \cap dom g)$
70	69 2	eleqtrrdi	$⊢ τ \to x \in D$
71	70	fvresd	$⊢ τ \to ({f ↾}_{D}) (x) = f (x)$
72	70	fvresd	$⊢ τ \to ({g ↾}_{D}) (x) = g (x)$
73	59 71 72	3eqtr3d	$⊢ τ \to f (x) = g (x)$
74	1	biimpi	$⊢ φ \to \forall f \in A Fun f$
75	3 74	bnj832	$⊢ ψ \to \forall f \in A Fun f$
76	4 75	bnj835	$⊢ χ \to \forall f \in A Fun f$
77	5 76	bnj835	$⊢ θ \to \forall f \in A Fun f$
78	6 77	bnj835	$⊢ τ \to \forall f \in A Fun f$
79	78 55	bnj1294	$⊢ τ \to Fun f$
80		funopfv	$⊢ Fun f \to (⟨x, y⟩ \in f \to f (x) = y)$
81	79 61 80	sylc	$⊢ τ \to f (x) = y$
82		funeq	$⊢ f = g \to (Fun f \leftrightarrow Fun g)$
83	82 78 57	rspcdva	$⊢ τ \to Fun g$
84	6	simp3bi	$⊢ τ \to ⟨x, z⟩ \in g$
85		funopfv	$⊢ Fun g \to (⟨x, z⟩ \in g \to g (x) = z)$
86	83 84 85	sylc	$⊢ τ \to g (x) = z$
87	73 81 86	3eqtr3d	$⊢ τ \to y = z$
88	50 87	bnj593	$⊢ θ \to \exists g y = z$
89	88	bnj937	$⊢ θ \to y = z$
90	30 89	bnj593	$⊢ χ \to \exists f y = z$
91	90	bnj937	$⊢ χ \to y = z$
92	4 91	sylbir	$⊢ (ψ \land ⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z$
93	92	3expib	$⊢ ψ \to ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z)$
94	93	alrimivv	$⊢ ψ \to \forall y \forall z ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z)$
95	94	alrimiv	$⊢ ψ \to \forall x \forall y \forall z ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z)$
96		dffun4	$⊢ Fun ⋃ A \leftrightarrow (Rel ⋃ A \land \forall x \forall y \forall z ((⟨x, y⟩ \in ⋃ A \land ⟨x, z⟩ \in ⋃ A) \to y = z))$
97	20 95 96	sylanbrc	$⊢ ψ \to Fun ⋃ A$

Metamath Proof Explorer

Theorem bnj1379

Proof