Theorem bnj1379

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

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

Proof

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