Theorem bnj1379 35227

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 35179	. . . . . . 7 ⊢ (𝜑 → ∀𝑓𝜑)
4	3	nf5i 2180	. . . . . 6 ⊢ Ⅎ𝑓𝜑
5		nfra1 3288	. . . . . 6 ⊢ Ⅎ𝑓∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
6	4, 5	nfan 1928	. . . . 5 ⊢ Ⅎ𝑓(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
7	1, 6	nfxfr 1882	. . . 4 ⊢ Ⅎ𝑓𝜓
8	2	bnj946 35172	. . . . . . . 8 ⊢ (𝜑 ↔ ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
9	8	biimpi 219	. . . . . . 7 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
10	9	19.21bi 2224	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ 𝐴 → Fun 𝑓))
11	1, 10	bnj832 35156	. . . . 5 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Fun 𝑓))
12		funrel 6553	. . . . 5 ⊢ (Fun 𝑓 → Rel 𝑓)
13	11, 12	syl6 36	. . . 4 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Rel 𝑓))
14	7, 13	ralrimi 3262	. . 3 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Rel 𝑓)
15		reluni 5804	. . 3 ⊢ (Rel ∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓)
16	14, 15	sylibr 237	. 2 ⊢ (𝜓 → Rel ∪ 𝐴)
17		bnj1379.5	. . . . . 6 ⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴))
18		eluni2 4875	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
19	18	biimpi 219	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
20	19	bnj1196 35191	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
21	17, 20	bnj836 35158	. . . . . . . . 9 ⊢ (𝜒 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22		bnj1379.6	. . . . . . . . 9 ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23		nfv 1943	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
24		nfv 1943	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
25	7, 23, 24	nf3an 1930	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
26	17, 25	nfxfr 1882	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜒
27	26	nf5ri 2230	. . . . . . . . 9 ⊢ (𝜒 → ∀𝑓𝜒)
28	21, 22, 27	bnj1345 35221	. . . . . . . 8 ⊢ (𝜒 → ∃𝑓𝜃)
29	17	simp3bi 1164	. . . . . . . . . . . . 13 ⊢ (𝜒 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
30	22, 29	bnj835 35157	. . . . . . . . . . . 12 ⊢ (𝜃 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
31		eluni2 4875	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
32	31	biimpi 219	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
33	32	bnj1196 35191	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
34	30, 33	syl 18	. . . . . . . . . . 11 ⊢ (𝜃 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35		bnj1379.7	. . . . . . . . . . 11 ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36		nfv 1943	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔𝜑
37		nfra2w 3300	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
38	36, 37	nfan 1928	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑔(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
39	1, 38	nfxfr 1882	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔𝜓
40		nfv 1943	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
41		nfv 1943	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
42	39, 40, 41	nf3an 1930	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
43	17, 42	nfxfr 1882	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝜒
44		nfv 1943	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔 𝑓 ∈ 𝐴
45		nfv 1943	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ 𝑓
46	43, 44, 45	nf3an 1930	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔(𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
47	22, 46	nfxfr 1882	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝜃
48	47	nf5ri 2230	. . . . . . . . . . 11 ⊢ (𝜃 → ∀𝑔𝜃)
49	34, 35, 48	bnj1345 35221	. . . . . . . . . 10 ⊢ (𝜃 → ∃𝑔𝜏)
50	1	simprbi 502	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
51	17, 50	bnj835 35157	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
52	22, 51	bnj835 35157	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
53	35, 52	bnj835 35157	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
54	22, 35	bnj1219 35197	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑓 ∈ 𝐴)
55	53, 54	bnj1294 35214	. . . . . . . . . . . . . 14 ⊢ (𝜏 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
56	35	simp2bi 1163	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑔 ∈ 𝐴)
57	55, 56	bnj1294 35214	. . . . . . . . . . . . 13 ⊢ (𝜏 → (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
58	57	fveq1d 6883	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = ((𝑔 ↾ 𝐷)‘𝑥))
59	22	simp3bi 1164	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
60	35, 59	bnj835 35157	. . . . . . . . . . . . . . . 16 ⊢ (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61		vex 3458	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
62		vex 3458	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
63	61, 62	opeldm 5896	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑓 → 𝑥 ∈ dom 𝑓)
64	60, 63	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑓)
65		vex 3458	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
66	61, 65	opeldm 5896	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝑔 → 𝑥 ∈ dom 𝑔)
67	35, 66	bnj837 35159	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑔)
68	64, 67	elind 4152	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69		bnj1379.2	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)
70	68, 69	eleqtrrdi 2873	. . . . . . . . . . . . 13 ⊢ (𝜏 → 𝑥 ∈ 𝐷)
71	70	fvresd 6901	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥))
72	70	fvresd 6901	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
73	58, 71, 72	3eqtr3d 2805	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = (𝑔‘𝑥))
74	2	biimpi 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
75	1, 74	bnj832 35156	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
76	17, 75	bnj835 35157	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
77	22, 76	bnj835 35157	. . . . . . . . . . . . . 14 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
78	35, 77	bnj835 35157	. . . . . . . . . . . . 13 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
79	78, 54	bnj1294 35214	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑓)
80		funopfv 6930	. . . . . . . . . . . 12 ⊢ (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓‘𝑥) = 𝑦))
81	79, 60, 80	sylc 66	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = 𝑦)
82		funeq 6556	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
83	82, 78, 56	rspcdva 3581	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑔)
84	35	simp3bi 1164	. . . . . . . . . . . 12 ⊢ (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
85		funopfv 6930	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔‘𝑥) = 𝑧))
86	83, 84, 85	sylc 66	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑔‘𝑥) = 𝑧)
87	73, 81, 86	3eqtr3d 2805	. . . . . . . . . 10 ⊢ (𝜏 → 𝑦 = 𝑧)
88	49, 87	bnj593 35143	. . . . . . . . 9 ⊢ (𝜃 → ∃𝑔 𝑦 = 𝑧)
89	88	bnj937 35169	. . . . . . . 8 ⊢ (𝜃 → 𝑦 = 𝑧)
90	28, 89	bnj593 35143	. . . . . . 7 ⊢ (𝜒 → ∃𝑓 𝑦 = 𝑧)
91	90	bnj937 35169	. . . . . 6 ⊢ (𝜒 → 𝑦 = 𝑧)
92	17, 91	sylbir 238	. . . . 5 ⊢ ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)
93	92	3expib 1139	. . . 4 ⊢ (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
94	93	alrimivv 1957	. . 3 ⊢ (𝜓 → ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
95	94	alrimiv 1956	. 2 ⊢ (𝜓 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
96		dffun4 6549	. 2 ⊢ (Fun ∪ 𝐴 ↔ (Rel ∪ 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)))
97	16, 95, 96	sylanbrc 594	1 ⊢ (𝜓 → Fun ∪ 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102  ∀wal 1567   = wceq 1569  ∃wex 1808   ∈ wcel 2142  ∀wral 3078  ∃wrex 3088   ∩ cin 3903  ⟨cop 4594  ∪ cuni 4871  dom cdm 5660   ↾ cres 5662  Rel wrel 5665  Fun wfun 6530  ‘cfv 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-res 5672  df-iota 6492  df-fun 6538  df-fv 6544

This theorem is used by:  bnj1383  35228