This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∪ 𝐴 )