Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1379 Structured version   Visualization version   GIF version

Theorem bnj1379 31229
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
StepHypRef Expression
1 bnj1379.3 . . . . 5 (𝜓 ↔ (𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)))
2 bnj1379.1 . . . . . . . 8 (𝜑 ↔ ∀𝑓𝐴 Fun 𝑓)
32bnj1095 31180 . . . . . . 7 (𝜑 → ∀𝑓𝜑)
43nf5i 2191 . . . . . 6 𝑓𝜑
5 nfra1 3136 . . . . . 6 𝑓𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
64, 5nfan 1990 . . . . 5 𝑓(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
71, 6nfxfr 1938 . . . 4 𝑓𝜓
82bnj946 31173 . . . . . . . 8 (𝜑 ↔ ∀𝑓(𝑓𝐴 → Fun 𝑓))
98biimpi 207 . . . . . . 7 (𝜑 → ∀𝑓(𝑓𝐴 → Fun 𝑓))
10919.21bi 2225 . . . . . 6 (𝜑 → (𝑓𝐴 → Fun 𝑓))
111, 10bnj832 31156 . . . . 5 (𝜓 → (𝑓𝐴 → Fun 𝑓))
12 funrel 6121 . . . . 5 (Fun 𝑓 → Rel 𝑓)
1311, 12syl6 35 . . . 4 (𝜓 → (𝑓𝐴 → Rel 𝑓))
147, 13ralrimi 3152 . . 3 (𝜓 → ∀𝑓𝐴 Rel 𝑓)
15 reluni 5450 . . 3 (Rel 𝐴 ↔ ∀𝑓𝐴 Rel 𝑓)
1614, 15sylibr 225 . 2 (𝜓 → Rel 𝐴)
17 bnj1379.5 . . . . . 6 (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴))
18 eluni2 4641 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
1918biimpi 207 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
2019bnj1196 31193 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
2117, 20bnj836 31158 . . . . . . . . 9 (𝜒 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22 bnj1379.6 . . . . . . . . 9 (𝜃 ↔ (𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23 nfv 2005 . . . . . . . . . . . 12 𝑓𝑥, 𝑦⟩ ∈ 𝐴
24 nfv 2005 . . . . . . . . . . . 12 𝑓𝑥, 𝑧⟩ ∈ 𝐴
257, 23, 24nf3an 1993 . . . . . . . . . . 11 𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
2617, 25nfxfr 1938 . . . . . . . . . 10 𝑓𝜒
2726nf5ri 2231 . . . . . . . . 9 (𝜒 → ∀𝑓𝜒)
2821, 22, 27bnj1345 31223 . . . . . . . 8 (𝜒 → ∃𝑓𝜃)
2917simp3bi 1170 . . . . . . . . . . . . 13 (𝜒 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
3022, 29bnj835 31157 . . . . . . . . . . . 12 (𝜃 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
31 eluni2 4641 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑧⟩ ∈ 𝐴 ↔ ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3231biimpi 207 . . . . . . . . . . . . 13 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3332bnj1196 31193 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
3430, 33syl 17 . . . . . . . . . . 11 (𝜃 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35 bnj1379.7 . . . . . . . . . . 11 (𝜏 ↔ (𝜃𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36 nfv 2005 . . . . . . . . . . . . . . . . . 18 𝑔𝜑
37 nfra2 3141 . . . . . . . . . . . . . . . . . 18 𝑔𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
3836, 37nfan 1990 . . . . . . . . . . . . . . . . 17 𝑔(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
391, 38nfxfr 1938 . . . . . . . . . . . . . . . 16 𝑔𝜓
40 nfv 2005 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑦⟩ ∈ 𝐴
41 nfv 2005 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑧⟩ ∈ 𝐴
4239, 40, 41nf3an 1993 . . . . . . . . . . . . . . 15 𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
4317, 42nfxfr 1938 . . . . . . . . . . . . . 14 𝑔𝜒
44 nfv 2005 . . . . . . . . . . . . . 14 𝑔 𝑓𝐴
45 nfv 2005 . . . . . . . . . . . . . 14 𝑔𝑥, 𝑦⟩ ∈ 𝑓
4643, 44, 45nf3an 1993 . . . . . . . . . . . . 13 𝑔(𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
4722, 46nfxfr 1938 . . . . . . . . . . . 12 𝑔𝜃
4847nf5ri 2231 . . . . . . . . . . 11 (𝜃 → ∀𝑔𝜃)
4934, 35, 48bnj1345 31223 . . . . . . . . . 10 (𝜃 → ∃𝑔𝜏)
501simprbi 486 . . . . . . . . . . . . . . . . . 18 (𝜓 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5117, 50bnj835 31157 . . . . . . . . . . . . . . . . 17 (𝜒 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5222, 51bnj835 31157 . . . . . . . . . . . . . . . 16 (𝜃 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5335, 52bnj835 31157 . . . . . . . . . . . . . . 15 (𝜏 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5422, 35bnj1219 31199 . . . . . . . . . . . . . . 15 (𝜏𝑓𝐴)
5553, 54bnj1294 31216 . . . . . . . . . . . . . 14 (𝜏 → ∀𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5635simp2bi 1169 . . . . . . . . . . . . . 14 (𝜏𝑔𝐴)
5755, 56bnj1294 31216 . . . . . . . . . . . . 13 (𝜏 → (𝑓𝐷) = (𝑔𝐷))
5857fveq1d 6413 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = ((𝑔𝐷)‘𝑥))
5922simp3bi 1170 . . . . . . . . . . . . . . . . 17 (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
6035, 59bnj835 31157 . . . . . . . . . . . . . . . 16 (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61 vex 3401 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
62 vex 3401 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
6361, 62opeldm 5536 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑓𝑥 ∈ dom 𝑓)
6460, 63syl 17 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑓)
65 vex 3401 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6661, 65opeldm 5536 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑧⟩ ∈ 𝑔𝑥 ∈ dom 𝑔)
6735, 66bnj837 31159 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑔)
6864, 67elind 4004 . . . . . . . . . . . . . 14 (𝜏𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69 bnj1379.2 . . . . . . . . . . . . . 14 𝐷 = (dom 𝑓 ∩ dom 𝑔)
7068, 69syl6eleqr 2903 . . . . . . . . . . . . 13 (𝜏𝑥𝐷)
71 fvres 6430 . . . . . . . . . . . . 13 (𝑥𝐷 → ((𝑓𝐷)‘𝑥) = (𝑓𝑥))
7270, 71syl 17 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = (𝑓𝑥))
73 fvres 6430 . . . . . . . . . . . . 13 (𝑥𝐷 → ((𝑔𝐷)‘𝑥) = (𝑔𝑥))
7470, 73syl 17 . . . . . . . . . . . 12 (𝜏 → ((𝑔𝐷)‘𝑥) = (𝑔𝑥))
7558, 72, 743eqtr3d 2855 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = (𝑔𝑥))
762biimpi 207 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑓𝐴 Fun 𝑓)
771, 76bnj832 31156 . . . . . . . . . . . . . . . 16 (𝜓 → ∀𝑓𝐴 Fun 𝑓)
7817, 77bnj835 31157 . . . . . . . . . . . . . . 15 (𝜒 → ∀𝑓𝐴 Fun 𝑓)
7922, 78bnj835 31157 . . . . . . . . . . . . . 14 (𝜃 → ∀𝑓𝐴 Fun 𝑓)
8035, 79bnj835 31157 . . . . . . . . . . . . 13 (𝜏 → ∀𝑓𝐴 Fun 𝑓)
8180, 54bnj1294 31216 . . . . . . . . . . . 12 (𝜏 → Fun 𝑓)
82 funopfv 6458 . . . . . . . . . . . 12 (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓𝑥) = 𝑦))
8381, 60, 82sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = 𝑦)
84 funeq 6124 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
8584cbvralv 3367 . . . . . . . . . . . . . 14 (∀𝑓𝐴 Fun 𝑓 ↔ ∀𝑔𝐴 Fun 𝑔)
8680, 85sylib 209 . . . . . . . . . . . . 13 (𝜏 → ∀𝑔𝐴 Fun 𝑔)
8786, 56bnj1294 31216 . . . . . . . . . . . 12 (𝜏 → Fun 𝑔)
8835simp3bi 1170 . . . . . . . . . . . 12 (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
89 funopfv 6458 . . . . . . . . . . . 12 (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔𝑥) = 𝑧))
9087, 88, 89sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑔𝑥) = 𝑧)
9175, 83, 903eqtr3d 2855 . . . . . . . . . 10 (𝜏𝑦 = 𝑧)
9249, 91bnj593 31143 . . . . . . . . 9 (𝜃 → ∃𝑔 𝑦 = 𝑧)
9392bnj937 31170 . . . . . . . 8 (𝜃𝑦 = 𝑧)
9428, 93bnj593 31143 . . . . . . 7 (𝜒 → ∃𝑓 𝑦 = 𝑧)
9594bnj937 31170 . . . . . 6 (𝜒𝑦 = 𝑧)
9617, 95sylbir 226 . . . . 5 ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)
97963expib 1145 . . . 4 (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9897alrimivv 2019 . . 3 (𝜓 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9998alrimiv 2018 . 2 (𝜓 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
100 dffun4 6116 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)))
10116, 99, 100sylanbrc 574 1 (𝜓 → Fun 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100  wal 1635   = wceq 1637  wex 1859  wcel 2157  wral 3103  wrex 3104  cin 3775  cop 4383   cuni 4637  dom cdm 5318  cres 5320  Rel wrel 5323  Fun wfun 6098  cfv 6104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pr 5103
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-res 5330  df-iota 6067  df-fun 6106  df-fv 6112
This theorem is referenced by:  bnj1383  31230
  Copyright terms: Public domain W3C validator