Theorem bnj1379 34844

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

Hypotheses

Ref	Expression
bnj1379.1	⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)
bnj1379.2	⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)
bnj1379.3	⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))
bnj1379.5	⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴))
bnj1379.6	⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
bnj1379.7	⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))

Assertion

Ref	Expression
bnj1379	⊢ (𝜓 → Fun ∪ 𝐴)

Distinct variable groups:   𝐴,𝑓,𝑔,𝑥,𝑦,𝑧   𝑥,𝐷   𝜑,𝑔   𝜓,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑓)   𝜓(𝑓,𝑔)   𝜒(𝑥,𝑦,𝑧,𝑓,𝑔)   𝜃(𝑥,𝑦,𝑧,𝑓,𝑔)   𝜏(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐷(𝑦,𝑧,𝑓,𝑔)

Proof of Theorem bnj1379

Step	Hyp	Ref	Expression
1		bnj1379.3	. . . . 5 ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))
2		bnj1379.1	. . . . . . . 8 ⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)
3	2	bnj1095 34795	. . . . . . 7 ⊢ (𝜑 → ∀𝑓𝜑)
4	3	nf5i 2146	. . . . . 6 ⊢ Ⅎ𝑓𝜑
5		nfra1 3284	. . . . . 6 ⊢ Ⅎ𝑓∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
6	4, 5	nfan 1899	. . . . 5 ⊢ Ⅎ𝑓(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
7	1, 6	nfxfr 1853	. . . 4 ⊢ Ⅎ𝑓𝜓
8	2	bnj946 34788	. . . . . . . 8 ⊢ (𝜑 ↔ ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
9	8	biimpi 216	. . . . . . 7 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
10	9	19.21bi 2189	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ 𝐴 → Fun 𝑓))
11	1, 10	bnj832 34772	. . . . 5 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Fun 𝑓))
12		funrel 6583	. . . . 5 ⊢ (Fun 𝑓 → Rel 𝑓)
13	11, 12	syl6 35	. . . 4 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Rel 𝑓))
14	7, 13	ralrimi 3257	. . 3 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Rel 𝑓)
15		reluni 5828	. . 3 ⊢ (Rel ∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓)
16	14, 15	sylibr 234	. 2 ⊢ (𝜓 → Rel ∪ 𝐴)
17		bnj1379.5	. . . . . 6 ⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴))
18		eluni2 4911	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
19	18	biimpi 216	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
20	19	bnj1196 34808	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
21	17, 20	bnj836 34774	. . . . . . . . 9 ⊢ (𝜒 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22		bnj1379.6	. . . . . . . . 9 ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
24		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
25	7, 23, 24	nf3an 1901	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
26	17, 25	nfxfr 1853	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜒
27	26	nf5ri 2195	. . . . . . . . 9 ⊢ (𝜒 → ∀𝑓𝜒)
28	21, 22, 27	bnj1345 34838	. . . . . . . 8 ⊢ (𝜒 → ∃𝑓𝜃)
29	17	simp3bi 1148	. . . . . . . . . . . . 13 ⊢ (𝜒 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
30	22, 29	bnj835 34773	. . . . . . . . . . . 12 ⊢ (𝜃 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
31		eluni2 4911	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
32	31	biimpi 216	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
33	32	bnj1196 34808	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
34	30, 33	syl 17	. . . . . . . . . . 11 ⊢ (𝜃 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35		bnj1379.7	. . . . . . . . . . 11 ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36		nfv 1914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔𝜑
37		nfra2w 3299	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
38	36, 37	nfan 1899	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑔(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
39	1, 38	nfxfr 1853	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔𝜓
40		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
41		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
42	39, 40, 41	nf3an 1901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
43	17, 42	nfxfr 1853	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝜒
44		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔 𝑓 ∈ 𝐴
45		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ 𝑓
46	43, 44, 45	nf3an 1901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔(𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
47	22, 46	nfxfr 1853	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝜃
48	47	nf5ri 2195	. . . . . . . . . . 11 ⊢ (𝜃 → ∀𝑔𝜃)
49	34, 35, 48	bnj1345 34838	. . . . . . . . . 10 ⊢ (𝜃 → ∃𝑔𝜏)
50	1	simprbi 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
51	17, 50	bnj835 34773	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
52	22, 51	bnj835 34773	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
53	35, 52	bnj835 34773	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
54	22, 35	bnj1219 34814	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑓 ∈ 𝐴)
55	53, 54	bnj1294 34831	. . . . . . . . . . . . . 14 ⊢ (𝜏 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
56	35	simp2bi 1147	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑔 ∈ 𝐴)
57	55, 56	bnj1294 34831	. . . . . . . . . . . . 13 ⊢ (𝜏 → (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
58	57	fveq1d 6908	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = ((𝑔 ↾ 𝐷)‘𝑥))
59	22	simp3bi 1148	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
60	35, 59	bnj835 34773	. . . . . . . . . . . . . . . 16 ⊢ (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61		vex 3484	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
62		vex 3484	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
63	61, 62	opeldm 5918	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑓 → 𝑥 ∈ dom 𝑓)
64	60, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑓)
65		vex 3484	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
66	61, 65	opeldm 5918	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝑔 → 𝑥 ∈ dom 𝑔)
67	35, 66	bnj837 34775	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑔)
68	64, 67	elind 4200	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69		bnj1379.2	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)
70	68, 69	eleqtrrdi 2852	. . . . . . . . . . . . 13 ⊢ (𝜏 → 𝑥 ∈ 𝐷)
71	70	fvresd 6926	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥))
72	70	fvresd 6926	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
73	58, 71, 72	3eqtr3d 2785	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = (𝑔‘𝑥))
74	2	biimpi 216	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
75	1, 74	bnj832 34772	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
76	17, 75	bnj835 34773	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
77	22, 76	bnj835 34773	. . . . . . . . . . . . . 14 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
78	35, 77	bnj835 34773	. . . . . . . . . . . . 13 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
79	78, 54	bnj1294 34831	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑓)
80		funopfv 6958	. . . . . . . . . . . 12 ⊢ (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓‘𝑥) = 𝑦))
81	79, 60, 80	sylc 65	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = 𝑦)
82		funeq 6586	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
83	82, 78, 56	rspcdva 3623	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑔)
84	35	simp3bi 1148	. . . . . . . . . . . 12 ⊢ (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
85		funopfv 6958	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔‘𝑥) = 𝑧))
86	83, 84, 85	sylc 65	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑔‘𝑥) = 𝑧)
87	73, 81, 86	3eqtr3d 2785	. . . . . . . . . 10 ⊢ (𝜏 → 𝑦 = 𝑧)
88	49, 87	bnj593 34759	. . . . . . . . 9 ⊢ (𝜃 → ∃𝑔 𝑦 = 𝑧)
89	88	bnj937 34785	. . . . . . . 8 ⊢ (𝜃 → 𝑦 = 𝑧)
90	28, 89	bnj593 34759	. . . . . . 7 ⊢ (𝜒 → ∃𝑓 𝑦 = 𝑧)
91	90	bnj937 34785	. . . . . 6 ⊢ (𝜒 → 𝑦 = 𝑧)
92	17, 91	sylbir 235	. . . . 5 ⊢ ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)
93	92	3expib 1123	. . . 4 ⊢ (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
94	93	alrimivv 1928	. . 3 ⊢ (𝜓 → ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
95	94	alrimiv 1927	. 2 ⊢ (𝜓 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
96		dffun4 6577	. 2 ⊢ (Fun ∪ 𝐴 ↔ (Rel ∪ 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)))
97	16, 95, 96	sylanbrc 583	1 ⊢ (𝜓 → Fun ∪ 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070   ∩ cin 3950  ⟨cop 4632  ∪ cuni 4907  dom cdm 5685   ↾ cres 5687  Rel wrel 5690  Fun wfun 6555  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-res 5697  df-iota 6514  df-fun 6563  df-fv 6569

This theorem is referenced by:  bnj1383  34845