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 31239
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 31190 . . . . . . 7 (𝜑 → ∀𝑓𝜑)
43nf5i 2179 . . . . . 6 𝑓𝜑
5 nfra1 3090 . . . . . 6 𝑓𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
64, 5nfan 1980 . . . . 5 𝑓(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
71, 6nfxfr 1929 . . . 4 𝑓𝜓
82bnj946 31183 . . . . . . . 8 (𝜑 ↔ ∀𝑓(𝑓𝐴 → Fun 𝑓))
98biimpi 206 . . . . . . 7 (𝜑 → ∀𝑓(𝑓𝐴 → Fun 𝑓))
10919.21bi 2213 . . . . . 6 (𝜑 → (𝑓𝐴 → Fun 𝑓))
111, 10bnj832 31166 . . . . 5 (𝜓 → (𝑓𝐴 → Fun 𝑓))
12 funrel 6048 . . . . 5 (Fun 𝑓 → Rel 𝑓)
1311, 12syl6 35 . . . 4 (𝜓 → (𝑓𝐴 → Rel 𝑓))
147, 13ralrimi 3106 . . 3 (𝜓 → ∀𝑓𝐴 Rel 𝑓)
15 reluni 5380 . . 3 (Rel 𝐴 ↔ ∀𝑓𝐴 Rel 𝑓)
1614, 15sylibr 224 . 2 (𝜓 → Rel 𝐴)
17 bnj1379.5 . . . . . 6 (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴))
18 eluni2 4578 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
1918biimpi 206 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
2019bnj1196 31203 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
2117, 20bnj836 31168 . . . . . . . . 9 (𝜒 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22 bnj1379.6 . . . . . . . . 9 (𝜃 ↔ (𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23 nfv 1995 . . . . . . . . . . . 12 𝑓𝑥, 𝑦⟩ ∈ 𝐴
24 nfv 1995 . . . . . . . . . . . 12 𝑓𝑥, 𝑧⟩ ∈ 𝐴
257, 23, 24nf3an 1983 . . . . . . . . . . 11 𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
2617, 25nfxfr 1929 . . . . . . . . . 10 𝑓𝜒
2726nf5ri 2219 . . . . . . . . 9 (𝜒 → ∀𝑓𝜒)
2821, 22, 27bnj1345 31233 . . . . . . . 8 (𝜒 → ∃𝑓𝜃)
2917simp3bi 1141 . . . . . . . . . . . . 13 (𝜒 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
3022, 29bnj835 31167 . . . . . . . . . . . 12 (𝜃 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
31 eluni2 4578 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑧⟩ ∈ 𝐴 ↔ ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3231biimpi 206 . . . . . . . . . . . . 13 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3332bnj1196 31203 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
3430, 33syl 17 . . . . . . . . . . 11 (𝜃 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35 bnj1379.7 . . . . . . . . . . 11 (𝜏 ↔ (𝜃𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36 nfv 1995 . . . . . . . . . . . . . . . . . 18 𝑔𝜑
37 nfra2 3095 . . . . . . . . . . . . . . . . . 18 𝑔𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
3836, 37nfan 1980 . . . . . . . . . . . . . . . . 17 𝑔(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
391, 38nfxfr 1929 . . . . . . . . . . . . . . . 16 𝑔𝜓
40 nfv 1995 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑦⟩ ∈ 𝐴
41 nfv 1995 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑧⟩ ∈ 𝐴
4239, 40, 41nf3an 1983 . . . . . . . . . . . . . . 15 𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
4317, 42nfxfr 1929 . . . . . . . . . . . . . 14 𝑔𝜒
44 nfv 1995 . . . . . . . . . . . . . 14 𝑔 𝑓𝐴
45 nfv 1995 . . . . . . . . . . . . . 14 𝑔𝑥, 𝑦⟩ ∈ 𝑓
4643, 44, 45nf3an 1983 . . . . . . . . . . . . 13 𝑔(𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
4722, 46nfxfr 1929 . . . . . . . . . . . 12 𝑔𝜃
4847nf5ri 2219 . . . . . . . . . . 11 (𝜃 → ∀𝑔𝜃)
4934, 35, 48bnj1345 31233 . . . . . . . . . 10 (𝜃 → ∃𝑔𝜏)
501simprbi 484 . . . . . . . . . . . . . . . . . 18 (𝜓 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5117, 50bnj835 31167 . . . . . . . . . . . . . . . . 17 (𝜒 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5222, 51bnj835 31167 . . . . . . . . . . . . . . . 16 (𝜃 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5335, 52bnj835 31167 . . . . . . . . . . . . . . 15 (𝜏 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5422, 35bnj1219 31209 . . . . . . . . . . . . . . 15 (𝜏𝑓𝐴)
5553, 54bnj1294 31226 . . . . . . . . . . . . . 14 (𝜏 → ∀𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5635simp2bi 1140 . . . . . . . . . . . . . 14 (𝜏𝑔𝐴)
5755, 56bnj1294 31226 . . . . . . . . . . . . 13 (𝜏 → (𝑓𝐷) = (𝑔𝐷))
5857fveq1d 6334 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = ((𝑔𝐷)‘𝑥))
5922simp3bi 1141 . . . . . . . . . . . . . . . . 17 (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
6035, 59bnj835 31167 . . . . . . . . . . . . . . . 16 (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61 vex 3354 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
62 vex 3354 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
6361, 62opeldm 5466 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑓𝑥 ∈ dom 𝑓)
6460, 63syl 17 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑓)
65 vex 3354 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6661, 65opeldm 5466 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑧⟩ ∈ 𝑔𝑥 ∈ dom 𝑔)
6735, 66bnj837 31169 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑔)
6864, 67elind 3949 . . . . . . . . . . . . . 14 (𝜏𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69 bnj1379.2 . . . . . . . . . . . . . 14 𝐷 = (dom 𝑓 ∩ dom 𝑔)
7068, 69syl6eleqr 2861 . . . . . . . . . . . . 13 (𝜏𝑥𝐷)
71 fvres 6348 . . . . . . . . . . . . 13 (𝑥𝐷 → ((𝑓𝐷)‘𝑥) = (𝑓𝑥))
7270, 71syl 17 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = (𝑓𝑥))
73 fvres 6348 . . . . . . . . . . . . 13 (𝑥𝐷 → ((𝑔𝐷)‘𝑥) = (𝑔𝑥))
7470, 73syl 17 . . . . . . . . . . . 12 (𝜏 → ((𝑔𝐷)‘𝑥) = (𝑔𝑥))
7558, 72, 743eqtr3d 2813 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = (𝑔𝑥))
762biimpi 206 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑓𝐴 Fun 𝑓)
771, 76bnj832 31166 . . . . . . . . . . . . . . . 16 (𝜓 → ∀𝑓𝐴 Fun 𝑓)
7817, 77bnj835 31167 . . . . . . . . . . . . . . 15 (𝜒 → ∀𝑓𝐴 Fun 𝑓)
7922, 78bnj835 31167 . . . . . . . . . . . . . 14 (𝜃 → ∀𝑓𝐴 Fun 𝑓)
8035, 79bnj835 31167 . . . . . . . . . . . . 13 (𝜏 → ∀𝑓𝐴 Fun 𝑓)
8180, 54bnj1294 31226 . . . . . . . . . . . 12 (𝜏 → Fun 𝑓)
82 funopfv 6376 . . . . . . . . . . . 12 (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓𝑥) = 𝑦))
8381, 60, 82sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = 𝑦)
84 funeq 6051 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
8584cbvralv 3320 . . . . . . . . . . . . . 14 (∀𝑓𝐴 Fun 𝑓 ↔ ∀𝑔𝐴 Fun 𝑔)
8680, 85sylib 208 . . . . . . . . . . . . 13 (𝜏 → ∀𝑔𝐴 Fun 𝑔)
8786, 56bnj1294 31226 . . . . . . . . . . . 12 (𝜏 → Fun 𝑔)
8835simp3bi 1141 . . . . . . . . . . . 12 (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
89 funopfv 6376 . . . . . . . . . . . 12 (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔𝑥) = 𝑧))
9087, 88, 89sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑔𝑥) = 𝑧)
9175, 83, 903eqtr3d 2813 . . . . . . . . . 10 (𝜏𝑦 = 𝑧)
9249, 91bnj593 31153 . . . . . . . . 9 (𝜃 → ∃𝑔 𝑦 = 𝑧)
9392bnj937 31180 . . . . . . . 8 (𝜃𝑦 = 𝑧)
9428, 93bnj593 31153 . . . . . . 7 (𝜒 → ∃𝑓 𝑦 = 𝑧)
9594bnj937 31180 . . . . . 6 (𝜒𝑦 = 𝑧)
9617, 95sylbir 225 . . . . 5 ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)
97963expib 1116 . . . 4 (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9897alrimivv 2008 . . 3 (𝜓 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9998alrimiv 2007 . 2 (𝜓 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
100 dffun4 6043 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)))
10116, 99, 100sylanbrc 572 1 (𝜓 → Fun 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071  wal 1629   = wceq 1631  wex 1852  wcel 2145  wral 3061  wrex 3062  cin 3722  cop 4322   cuni 4574  dom cdm 5249  cres 5251  Rel wrel 5254  Fun wfun 6025  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-res 5261  df-iota 5994  df-fun 6033  df-fv 6039
This theorem is referenced by:  bnj1383  31240
  Copyright terms: Public domain W3C validator