Theorem bnj1379 34139

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 34090	. . . . . . 7 ⊢ (𝜑 → ∀𝑓𝜑)
4	3	nf5i 2140	. . . . . 6 ⊢ Ⅎ𝑓𝜑
5		nfra1 3279	. . . . . 6 ⊢ Ⅎ𝑓∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
6	4, 5	nfan 1900	. . . . 5 ⊢ Ⅎ𝑓(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
7	1, 6	nfxfr 1853	. . . 4 ⊢ Ⅎ𝑓𝜓
8	2	bnj946 34083	. . . . . . . 8 ⊢ (𝜑 ↔ ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
9	8	biimpi 215	. . . . . . 7 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
10	9	19.21bi 2180	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ 𝐴 → Fun 𝑓))
11	1, 10	bnj832 34067	. . . . 5 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Fun 𝑓))
12		funrel 6564	. . . . 5 ⊢ (Fun 𝑓 → Rel 𝑓)
13	11, 12	syl6 35	. . . 4 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Rel 𝑓))
14	7, 13	ralrimi 3252	. . 3 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Rel 𝑓)
15		reluni 5817	. . 3 ⊢ (Rel ∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓)
16	14, 15	sylibr 233	. 2 ⊢ (𝜓 → Rel ∪ 𝐴)
17		bnj1379.5	. . . . . 6 ⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴))
18		eluni2 4911	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
19	18	biimpi 215	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
20	19	bnj1196 34103	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
21	17, 20	bnj836 34069	. . . . . . . . 9 ⊢ (𝜒 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22		bnj1379.6	. . . . . . . . 9 ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
24		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
25	7, 23, 24	nf3an 1902	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
26	17, 25	nfxfr 1853	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜒
27	26	nf5ri 2186	. . . . . . . . 9 ⊢ (𝜒 → ∀𝑓𝜒)
28	21, 22, 27	bnj1345 34133	. . . . . . . 8 ⊢ (𝜒 → ∃𝑓𝜃)
29	17	simp3bi 1145	. . . . . . . . . . . . 13 ⊢ (𝜒 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
30	22, 29	bnj835 34068	. . . . . . . . . . . 12 ⊢ (𝜃 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
31		eluni2 4911	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
32	31	biimpi 215	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
33	32	bnj1196 34103	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
34	30, 33	syl 17	. . . . . . . . . . 11 ⊢ (𝜃 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35		bnj1379.7	. . . . . . . . . . 11 ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36		nfv 1915	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔𝜑
37		nfra2w 3294	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
38	36, 37	nfan 1900	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑔(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
39	1, 38	nfxfr 1853	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔𝜓
40		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
41		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
42	39, 40, 41	nf3an 1902	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
43	17, 42	nfxfr 1853	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝜒
44		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔 𝑓 ∈ 𝐴
45		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ 𝑓
46	43, 44, 45	nf3an 1902	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔(𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
47	22, 46	nfxfr 1853	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝜃
48	47	nf5ri 2186	. . . . . . . . . . 11 ⊢ (𝜃 → ∀𝑔𝜃)
49	34, 35, 48	bnj1345 34133	. . . . . . . . . 10 ⊢ (𝜃 → ∃𝑔𝜏)
50	1	simprbi 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
51	17, 50	bnj835 34068	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
52	22, 51	bnj835 34068	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
53	35, 52	bnj835 34068	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
54	22, 35	bnj1219 34109	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑓 ∈ 𝐴)
55	53, 54	bnj1294 34126	. . . . . . . . . . . . . 14 ⊢ (𝜏 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
56	35	simp2bi 1144	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑔 ∈ 𝐴)
57	55, 56	bnj1294 34126	. . . . . . . . . . . . 13 ⊢ (𝜏 → (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
58	57	fveq1d 6892	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = ((𝑔 ↾ 𝐷)‘𝑥))
59	22	simp3bi 1145	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
60	35, 59	bnj835 34068	. . . . . . . . . . . . . . . 16 ⊢ (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61		vex 3476	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
62		vex 3476	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
63	61, 62	opeldm 5906	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑓 → 𝑥 ∈ dom 𝑓)
64	60, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑓)
65		vex 3476	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
66	61, 65	opeldm 5906	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝑔 → 𝑥 ∈ dom 𝑔)
67	35, 66	bnj837 34070	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑔)
68	64, 67	elind 4193	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69		bnj1379.2	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)
70	68, 69	eleqtrrdi 2842	. . . . . . . . . . . . 13 ⊢ (𝜏 → 𝑥 ∈ 𝐷)
71	70	fvresd 6910	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥))
72	70	fvresd 6910	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
73	58, 71, 72	3eqtr3d 2778	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = (𝑔‘𝑥))
74	2	biimpi 215	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
75	1, 74	bnj832 34067	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
76	17, 75	bnj835 34068	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
77	22, 76	bnj835 34068	. . . . . . . . . . . . . 14 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
78	35, 77	bnj835 34068	. . . . . . . . . . . . 13 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
79	78, 54	bnj1294 34126	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑓)
80		funopfv 6942	. . . . . . . . . . . 12 ⊢ (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓‘𝑥) = 𝑦))
81	79, 60, 80	sylc 65	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = 𝑦)
82		funeq 6567	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
83	82, 78, 56	rspcdva 3612	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑔)
84	35	simp3bi 1145	. . . . . . . . . . . 12 ⊢ (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
85		funopfv 6942	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔‘𝑥) = 𝑧))
86	83, 84, 85	sylc 65	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑔‘𝑥) = 𝑧)
87	73, 81, 86	3eqtr3d 2778	. . . . . . . . . 10 ⊢ (𝜏 → 𝑦 = 𝑧)
88	49, 87	bnj593 34054	. . . . . . . . 9 ⊢ (𝜃 → ∃𝑔 𝑦 = 𝑧)
89	88	bnj937 34080	. . . . . . . 8 ⊢ (𝜃 → 𝑦 = 𝑧)
90	28, 89	bnj593 34054	. . . . . . 7 ⊢ (𝜒 → ∃𝑓 𝑦 = 𝑧)
91	90	bnj937 34080	. . . . . 6 ⊢ (𝜒 → 𝑦 = 𝑧)
92	17, 91	sylbir 234	. . . . 5 ⊢ ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)
93	92	3expib 1120	. . . 4 ⊢ (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
94	93	alrimivv 1929	. . 3 ⊢ (𝜓 → ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
95	94	alrimiv 1928	. 2 ⊢ (𝜓 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
96		dffun4 6558	. 2 ⊢ (Fun ∪ 𝐴 ↔ (Rel ∪ 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)))
97	16, 95, 96	sylanbrc 581	1 ⊢ (𝜓 → Fun ∪ 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085  ∀wal 1537   = wceq 1539  ∃wex 1779   ∈ wcel 2104  ∀wral 3059  ∃wrex 3068   ∩ cin 3946  ⟨cop 4633  ∪ cuni 4907  dom cdm 5675   ↾ cres 5677  Rel wrel 5680  Fun wfun 6536  ‘cfv 6542

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-res 5687  df-iota 6494  df-fun 6544  df-fv 6550

This theorem is referenced by:  bnj1383  34140