Theorem bnj1379 32710

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 32661	. . . . . . 7 ⊢ (𝜑 → ∀𝑓𝜑)
4	3	nf5i 2144	. . . . . 6 ⊢ Ⅎ𝑓𝜑
5		nfra1 3142	. . . . . 6 ⊢ Ⅎ𝑓∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
6	4, 5	nfan 1903	. . . . 5 ⊢ Ⅎ𝑓(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
7	1, 6	nfxfr 1856	. . . 4 ⊢ Ⅎ𝑓𝜓
8	2	bnj946 32654	. . . . . . . 8 ⊢ (𝜑 ↔ ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
9	8	biimpi 215	. . . . . . 7 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
10	9	19.21bi 2184	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ 𝐴 → Fun 𝑓))
11	1, 10	bnj832 32638	. . . . 5 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Fun 𝑓))
12		funrel 6435	. . . . 5 ⊢ (Fun 𝑓 → Rel 𝑓)
13	11, 12	syl6 35	. . . 4 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Rel 𝑓))
14	7, 13	ralrimi 3139	. . 3 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Rel 𝑓)
15		reluni 5717	. . 3 ⊢ (Rel ∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓)
16	14, 15	sylibr 233	. 2 ⊢ (𝜓 → Rel ∪ 𝐴)
17		bnj1379.5	. . . . . 6 ⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴))
18		eluni2 4840	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
19	18	biimpi 215	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
20	19	bnj1196 32674	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
21	17, 20	bnj836 32640	. . . . . . . . 9 ⊢ (𝜒 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22		bnj1379.6	. . . . . . . . 9 ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23		nfv 1918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
24		nfv 1918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
25	7, 23, 24	nf3an 1905	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
26	17, 25	nfxfr 1856	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜒
27	26	nf5ri 2191	. . . . . . . . 9 ⊢ (𝜒 → ∀𝑓𝜒)
28	21, 22, 27	bnj1345 32704	. . . . . . . 8 ⊢ (𝜒 → ∃𝑓𝜃)
29	17	simp3bi 1145	. . . . . . . . . . . . 13 ⊢ (𝜒 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
30	22, 29	bnj835 32639	. . . . . . . . . . . 12 ⊢ (𝜃 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
31		eluni2 4840	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
32	31	biimpi 215	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
33	32	bnj1196 32674	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
34	30, 33	syl 17	. . . . . . . . . . 11 ⊢ (𝜃 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35		bnj1379.7	. . . . . . . . . . 11 ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔𝜑
37		nfra2w 3151	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
38	36, 37	nfan 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑔(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
39	1, 38	nfxfr 1856	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔𝜓
40		nfv 1918	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
41		nfv 1918	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
42	39, 40, 41	nf3an 1905	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
43	17, 42	nfxfr 1856	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝜒
44		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔 𝑓 ∈ 𝐴
45		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ 𝑓
46	43, 44, 45	nf3an 1905	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔(𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
47	22, 46	nfxfr 1856	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝜃
48	47	nf5ri 2191	. . . . . . . . . . 11 ⊢ (𝜃 → ∀𝑔𝜃)
49	34, 35, 48	bnj1345 32704	. . . . . . . . . 10 ⊢ (𝜃 → ∃𝑔𝜏)
50	1	simprbi 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
51	17, 50	bnj835 32639	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
52	22, 51	bnj835 32639	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
53	35, 52	bnj835 32639	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
54	22, 35	bnj1219 32680	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑓 ∈ 𝐴)
55	53, 54	bnj1294 32697	. . . . . . . . . . . . . 14 ⊢ (𝜏 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
56	35	simp2bi 1144	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑔 ∈ 𝐴)
57	55, 56	bnj1294 32697	. . . . . . . . . . . . 13 ⊢ (𝜏 → (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
58	57	fveq1d 6758	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = ((𝑔 ↾ 𝐷)‘𝑥))
59	22	simp3bi 1145	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
60	35, 59	bnj835 32639	. . . . . . . . . . . . . . . 16 ⊢ (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61		vex 3426	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
62		vex 3426	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
63	61, 62	opeldm 5805	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑓 → 𝑥 ∈ dom 𝑓)
64	60, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑓)
65		vex 3426	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
66	61, 65	opeldm 5805	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝑔 → 𝑥 ∈ dom 𝑔)
67	35, 66	bnj837 32641	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑔)
68	64, 67	elind 4124	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69		bnj1379.2	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)
70	68, 69	eleqtrrdi 2850	. . . . . . . . . . . . 13 ⊢ (𝜏 → 𝑥 ∈ 𝐷)
71	70	fvresd 6776	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥))
72	70	fvresd 6776	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
73	58, 71, 72	3eqtr3d 2786	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = (𝑔‘𝑥))
74	2	biimpi 215	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
75	1, 74	bnj832 32638	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
76	17, 75	bnj835 32639	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
77	22, 76	bnj835 32639	. . . . . . . . . . . . . 14 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
78	35, 77	bnj835 32639	. . . . . . . . . . . . 13 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
79	78, 54	bnj1294 32697	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑓)
80		funopfv 6803	. . . . . . . . . . . 12 ⊢ (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓‘𝑥) = 𝑦))
81	79, 60, 80	sylc 65	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = 𝑦)
82		funeq 6438	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
83	82, 78, 56	rspcdva 3554	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑔)
84	35	simp3bi 1145	. . . . . . . . . . . 12 ⊢ (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
85		funopfv 6803	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔‘𝑥) = 𝑧))
86	83, 84, 85	sylc 65	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑔‘𝑥) = 𝑧)
87	73, 81, 86	3eqtr3d 2786	. . . . . . . . . 10 ⊢ (𝜏 → 𝑦 = 𝑧)
88	49, 87	bnj593 32625	. . . . . . . . 9 ⊢ (𝜃 → ∃𝑔 𝑦 = 𝑧)
89	88	bnj937 32651	. . . . . . . 8 ⊢ (𝜃 → 𝑦 = 𝑧)
90	28, 89	bnj593 32625	. . . . . . 7 ⊢ (𝜒 → ∃𝑓 𝑦 = 𝑧)
91	90	bnj937 32651	. . . . . 6 ⊢ (𝜒 → 𝑦 = 𝑧)
92	17, 91	sylbir 234	. . . . 5 ⊢ ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)
93	92	3expib 1120	. . . 4 ⊢ (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
94	93	alrimivv 1932	. . 3 ⊢ (𝜓 → ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
95	94	alrimiv 1931	. 2 ⊢ (𝜓 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
96		dffun4 6430	. 2 ⊢ (Fun ∪ 𝐴 ↔ (Rel ∪ 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)))
97	16, 95, 96	sylanbrc 582	1 ⊢ (𝜓 → Fun ∪ 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064   ∩ cin 3882  ⟨cop 4564  ∪ cuni 4836  dom cdm 5580   ↾ cres 5582  Rel wrel 5585  Fun wfun 6412  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-res 5592  df-iota 6376  df-fun 6420  df-fv 6426

This theorem is referenced by:  bnj1383  32711