Theorem bnj1379 30155

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 30106	. . . . . . 7 ⊢ (𝜑 → ∀𝑓𝜑)
4	3	nf5i 2011	. . . . . 6 ⊢ Ⅎ𝑓𝜑
5		nfra1 2925	. . . . . 6 ⊢ Ⅎ𝑓∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
6	4, 5	nfan 1816	. . . . 5 ⊢ Ⅎ𝑓(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
7	1, 6	nfxfr 1771	. . . 4 ⊢ Ⅎ𝑓𝜓
8	2	bnj946 30099	. . . . . . . 8 ⊢ (𝜑 ↔ ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
9	8	biimpi 205	. . . . . . 7 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓))
10	9	19.21bi 2047	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ 𝐴 → Fun 𝑓))
11	1, 10	bnj832 30082	. . . . 5 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Fun 𝑓))
12		funrel 5821	. . . . 5 ⊢ (Fun 𝑓 → Rel 𝑓)
13	11, 12	syl6 34	. . . 4 ⊢ (𝜓 → (𝑓 ∈ 𝐴 → Rel 𝑓))
14	7, 13	ralrimi 2940	. . 3 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Rel 𝑓)
15		reluni 5164	. . 3 ⊢ (Rel ∪ 𝐴 ↔ ∀𝑓 ∈ 𝐴 Rel 𝑓)
16	14, 15	sylibr 223	. 2 ⊢ (𝜓 → Rel ∪ 𝐴)
17		bnj1379.5	. . . . . 6 ⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴))
18		eluni2 4376	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ↔ ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
19	18	biimpi 205	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓 ∈ 𝐴 ⟨𝑥, 𝑦⟩ ∈ 𝑓)
20	19	bnj1196 30119	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
21	17, 20	bnj836 30084	. . . . . . . . 9 ⊢ (𝜒 → ∃𝑓(𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22		bnj1379.6	. . . . . . . . 9 ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23		nfv 1830	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
24		nfv 1830	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
25	7, 23, 24	nf3an 1819	. . . . . . . . . . 11 ⊢ Ⅎ𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
26	17, 25	nfxfr 1771	. . . . . . . . . 10 ⊢ Ⅎ𝑓𝜒
27	26	nf5ri 2053	. . . . . . . . 9 ⊢ (𝜒 → ∀𝑓𝜒)
28	21, 22, 27	bnj1345 30149	. . . . . . . 8 ⊢ (𝜒 → ∃𝑓𝜃)
29	17	simp3bi 1071	. . . . . . . . . . . . 13 ⊢ (𝜒 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
30	22, 29	bnj835 30083	. . . . . . . . . . . 12 ⊢ (𝜃 → ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
31		eluni2 4376	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
32	31	biimpi 205	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔 ∈ 𝐴 ⟨𝑥, 𝑧⟩ ∈ 𝑔)
33	32	bnj1196 30119	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
34	30, 33	syl 17	. . . . . . . . . . 11 ⊢ (𝜃 → ∃𝑔(𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35		bnj1379.7	. . . . . . . . . . 11 ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36		nfv 1830	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔𝜑
37		nfra2 2930	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑔∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)
38	36, 37	nfan 1816	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑔(𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
39	1, 38	nfxfr 1771	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔𝜓
40		nfv 1830	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴
41		nfv 1830	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑔⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴
42	39, 40, 41	nf3an 1819	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴)
43	17, 42	nfxfr 1771	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔𝜒
44		nfv 1830	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔 𝑓 ∈ 𝐴
45		nfv 1830	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔⟨𝑥, 𝑦⟩ ∈ 𝑓
46	43, 44, 45	nf3an 1819	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑔(𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
47	22, 46	nfxfr 1771	. . . . . . . . . . . 12 ⊢ Ⅎ𝑔𝜃
48	47	nf5ri 2053	. . . . . . . . . . 11 ⊢ (𝜃 → ∀𝑔𝜃)
49	34, 35, 48	bnj1345 30149	. . . . . . . . . 10 ⊢ (𝜃 → ∃𝑔𝜏)
50	1	simprbi 479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
51	17, 50	bnj835 30083	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
52	22, 51	bnj835 30083	. . . . . . . . . . . . . . . 16 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
53	35, 52	bnj835 30083	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
54	22, 35	bnj1219 30125	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑓 ∈ 𝐴)
55	53, 54	bnj1294 30142	. . . . . . . . . . . . . 14 ⊢ (𝜏 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
56	35	simp2bi 1070	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑔 ∈ 𝐴)
57	55, 56	bnj1294 30142	. . . . . . . . . . . . 13 ⊢ (𝜏 → (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))
58	57	fveq1d 6105	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = ((𝑔 ↾ 𝐷)‘𝑥))
59	22	simp3bi 1071	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
60	35, 59	bnj835 30083	. . . . . . . . . . . . . . . 16 ⊢ (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
62		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
63	61, 62	opeldm 5250	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑓 → 𝑥 ∈ dom 𝑓)
64	60, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑓)
65		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
66	61, 65	opeldm 5250	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝑔 → 𝑥 ∈ dom 𝑔)
67	35, 66	bnj837 30085	. . . . . . . . . . . . . . 15 ⊢ (𝜏 → 𝑥 ∈ dom 𝑔)
68	64, 67	elind 3760	. . . . . . . . . . . . . 14 ⊢ (𝜏 → 𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69		bnj1379.2	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)
70	68, 69	syl6eleqr 2699	. . . . . . . . . . . . 13 ⊢ (𝜏 → 𝑥 ∈ 𝐷)
71		fvres 6117	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥))
72	70, 71	syl 17	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑓 ↾ 𝐷)‘𝑥) = (𝑓‘𝑥))
73		fvres 6117	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
74	70, 73	syl 17	. . . . . . . . . . . 12 ⊢ (𝜏 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
75	58, 72, 74	3eqtr3d 2652	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = (𝑔‘𝑥))
76	2	biimpi 205	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
77	1, 76	bnj832 30082	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
78	17, 77	bnj835 30083	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
79	22, 78	bnj835 30083	. . . . . . . . . . . . . 14 ⊢ (𝜃 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
80	35, 79	bnj835 30083	. . . . . . . . . . . . 13 ⊢ (𝜏 → ∀𝑓 ∈ 𝐴 Fun 𝑓)
81	80, 54	bnj1294 30142	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑓)
82		funopfv 6145	. . . . . . . . . . . 12 ⊢ (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓‘𝑥) = 𝑦))
83	81, 60, 82	sylc 63	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑓‘𝑥) = 𝑦)
84		funeq 5823	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
85	84	cbvralv 3147	. . . . . . . . . . . . . 14 ⊢ (∀𝑓 ∈ 𝐴 Fun 𝑓 ↔ ∀𝑔 ∈ 𝐴 Fun 𝑔)
86	80, 85	sylib 207	. . . . . . . . . . . . 13 ⊢ (𝜏 → ∀𝑔 ∈ 𝐴 Fun 𝑔)
87	86, 56	bnj1294 30142	. . . . . . . . . . . 12 ⊢ (𝜏 → Fun 𝑔)
88	35	simp3bi 1071	. . . . . . . . . . . 12 ⊢ (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
89		funopfv 6145	. . . . . . . . . . . 12 ⊢ (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔‘𝑥) = 𝑧))
90	87, 88, 89	sylc 63	. . . . . . . . . . 11 ⊢ (𝜏 → (𝑔‘𝑥) = 𝑧)
91	75, 83, 90	3eqtr3d 2652	. . . . . . . . . 10 ⊢ (𝜏 → 𝑦 = 𝑧)
92	49, 91	bnj593 30069	. . . . . . . . 9 ⊢ (𝜃 → ∃𝑔 𝑦 = 𝑧)
93	92	bnj937 30096	. . . . . . . 8 ⊢ (𝜃 → 𝑦 = 𝑧)
94	28, 93	bnj593 30069	. . . . . . 7 ⊢ (𝜒 → ∃𝑓 𝑦 = 𝑧)
95	94	bnj937 30096	. . . . . 6 ⊢ (𝜒 → 𝑦 = 𝑧)
96	17, 95	sylbir 224	. . . . 5 ⊢ ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)
97	96	3expib 1260	. . . 4 ⊢ (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
98	97	alrimivv 1843	. . 3 ⊢ (𝜓 → ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
99	98	alrimiv 1842	. 2 ⊢ (𝜓 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧))
100		dffun4 5816	. 2 ⊢ (Fun ∪ 𝐴 ↔ (Rel ∪ 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴) → 𝑦 = 𝑧)))
101	16, 99, 100	sylanbrc 695	1 ⊢ (𝜓 → Fun ∪ 𝐴)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ∩ cin 3539  ⟨cop 4131  ∪ cuni 4372  dom cdm 5038   ↾ cres 5040  Rel wrel 5043  Fun wfun 5798  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-res 5050  df-iota 5768  df-fun 5806  df-fv 5812

This theorem is referenced by:  bnj1383  30156