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 30875
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 30826 . . . . . . 7 (𝜑 → ∀𝑓𝜑)
43nf5i 2022 . . . . . 6 𝑓𝜑
5 nfra1 2938 . . . . . 6 𝑓𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
64, 5nfan 1826 . . . . 5 𝑓(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
71, 6nfxfr 1777 . . . 4 𝑓𝜓
82bnj946 30819 . . . . . . . 8 (𝜑 ↔ ∀𝑓(𝑓𝐴 → Fun 𝑓))
98biimpi 206 . . . . . . 7 (𝜑 → ∀𝑓(𝑓𝐴 → Fun 𝑓))
10919.21bi 2057 . . . . . 6 (𝜑 → (𝑓𝐴 → Fun 𝑓))
111, 10bnj832 30802 . . . . 5 (𝜓 → (𝑓𝐴 → Fun 𝑓))
12 funrel 5893 . . . . 5 (Fun 𝑓 → Rel 𝑓)
1311, 12syl6 35 . . . 4 (𝜓 → (𝑓𝐴 → Rel 𝑓))
147, 13ralrimi 2954 . . 3 (𝜓 → ∀𝑓𝐴 Rel 𝑓)
15 reluni 5231 . . 3 (Rel 𝐴 ↔ ∀𝑓𝐴 Rel 𝑓)
1614, 15sylibr 224 . 2 (𝜓 → Rel 𝐴)
17 bnj1379.5 . . . . . 6 (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴))
18 eluni2 4431 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
1918biimpi 206 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
2019bnj1196 30839 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
2117, 20bnj836 30804 . . . . . . . . 9 (𝜒 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22 bnj1379.6 . . . . . . . . 9 (𝜃 ↔ (𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23 nfv 1841 . . . . . . . . . . . 12 𝑓𝑥, 𝑦⟩ ∈ 𝐴
24 nfv 1841 . . . . . . . . . . . 12 𝑓𝑥, 𝑧⟩ ∈ 𝐴
257, 23, 24nf3an 1829 . . . . . . . . . . 11 𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
2617, 25nfxfr 1777 . . . . . . . . . 10 𝑓𝜒
2726nf5ri 2063 . . . . . . . . 9 (𝜒 → ∀𝑓𝜒)
2821, 22, 27bnj1345 30869 . . . . . . . 8 (𝜒 → ∃𝑓𝜃)
2917simp3bi 1076 . . . . . . . . . . . . 13 (𝜒 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
3022, 29bnj835 30803 . . . . . . . . . . . 12 (𝜃 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
31 eluni2 4431 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑧⟩ ∈ 𝐴 ↔ ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3231biimpi 206 . . . . . . . . . . . . 13 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3332bnj1196 30839 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
3430, 33syl 17 . . . . . . . . . . 11 (𝜃 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35 bnj1379.7 . . . . . . . . . . 11 (𝜏 ↔ (𝜃𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36 nfv 1841 . . . . . . . . . . . . . . . . . 18 𝑔𝜑
37 nfra2 2943 . . . . . . . . . . . . . . . . . 18 𝑔𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
3836, 37nfan 1826 . . . . . . . . . . . . . . . . 17 𝑔(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
391, 38nfxfr 1777 . . . . . . . . . . . . . . . 16 𝑔𝜓
40 nfv 1841 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑦⟩ ∈ 𝐴
41 nfv 1841 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑧⟩ ∈ 𝐴
4239, 40, 41nf3an 1829 . . . . . . . . . . . . . . 15 𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
4317, 42nfxfr 1777 . . . . . . . . . . . . . 14 𝑔𝜒
44 nfv 1841 . . . . . . . . . . . . . 14 𝑔 𝑓𝐴
45 nfv 1841 . . . . . . . . . . . . . 14 𝑔𝑥, 𝑦⟩ ∈ 𝑓
4643, 44, 45nf3an 1829 . . . . . . . . . . . . 13 𝑔(𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
4722, 46nfxfr 1777 . . . . . . . . . . . 12 𝑔𝜃
4847nf5ri 2063 . . . . . . . . . . 11 (𝜃 → ∀𝑔𝜃)
4934, 35, 48bnj1345 30869 . . . . . . . . . 10 (𝜃 → ∃𝑔𝜏)
501simprbi 480 . . . . . . . . . . . . . . . . . 18 (𝜓 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5117, 50bnj835 30803 . . . . . . . . . . . . . . . . 17 (𝜒 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5222, 51bnj835 30803 . . . . . . . . . . . . . . . 16 (𝜃 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5335, 52bnj835 30803 . . . . . . . . . . . . . . 15 (𝜏 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5422, 35bnj1219 30845 . . . . . . . . . . . . . . 15 (𝜏𝑓𝐴)
5553, 54bnj1294 30862 . . . . . . . . . . . . . 14 (𝜏 → ∀𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5635simp2bi 1075 . . . . . . . . . . . . . 14 (𝜏𝑔𝐴)
5755, 56bnj1294 30862 . . . . . . . . . . . . 13 (𝜏 → (𝑓𝐷) = (𝑔𝐷))
5857fveq1d 6180 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = ((𝑔𝐷)‘𝑥))
5922simp3bi 1076 . . . . . . . . . . . . . . . . 17 (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
6035, 59bnj835 30803 . . . . . . . . . . . . . . . 16 (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61 vex 3198 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
62 vex 3198 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
6361, 62opeldm 5317 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑓𝑥 ∈ dom 𝑓)
6460, 63syl 17 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑓)
65 vex 3198 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6661, 65opeldm 5317 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑧⟩ ∈ 𝑔𝑥 ∈ dom 𝑔)
6735, 66bnj837 30805 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑔)
6864, 67elind 3790 . . . . . . . . . . . . . 14 (𝜏𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69 bnj1379.2 . . . . . . . . . . . . . 14 𝐷 = (dom 𝑓 ∩ dom 𝑔)
7068, 69syl6eleqr 2710 . . . . . . . . . . . . 13 (𝜏𝑥𝐷)
71 fvres 6194 . . . . . . . . . . . . 13 (𝑥𝐷 → ((𝑓𝐷)‘𝑥) = (𝑓𝑥))
7270, 71syl 17 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = (𝑓𝑥))
73 fvres 6194 . . . . . . . . . . . . 13 (𝑥𝐷 → ((𝑔𝐷)‘𝑥) = (𝑔𝑥))
7470, 73syl 17 . . . . . . . . . . . 12 (𝜏 → ((𝑔𝐷)‘𝑥) = (𝑔𝑥))
7558, 72, 743eqtr3d 2662 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = (𝑔𝑥))
762biimpi 206 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑓𝐴 Fun 𝑓)
771, 76bnj832 30802 . . . . . . . . . . . . . . . 16 (𝜓 → ∀𝑓𝐴 Fun 𝑓)
7817, 77bnj835 30803 . . . . . . . . . . . . . . 15 (𝜒 → ∀𝑓𝐴 Fun 𝑓)
7922, 78bnj835 30803 . . . . . . . . . . . . . 14 (𝜃 → ∀𝑓𝐴 Fun 𝑓)
8035, 79bnj835 30803 . . . . . . . . . . . . 13 (𝜏 → ∀𝑓𝐴 Fun 𝑓)
8180, 54bnj1294 30862 . . . . . . . . . . . 12 (𝜏 → Fun 𝑓)
82 funopfv 6222 . . . . . . . . . . . 12 (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓𝑥) = 𝑦))
8381, 60, 82sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = 𝑦)
84 funeq 5896 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
8584cbvralv 3166 . . . . . . . . . . . . . 14 (∀𝑓𝐴 Fun 𝑓 ↔ ∀𝑔𝐴 Fun 𝑔)
8680, 85sylib 208 . . . . . . . . . . . . 13 (𝜏 → ∀𝑔𝐴 Fun 𝑔)
8786, 56bnj1294 30862 . . . . . . . . . . . 12 (𝜏 → Fun 𝑔)
8835simp3bi 1076 . . . . . . . . . . . 12 (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
89 funopfv 6222 . . . . . . . . . . . 12 (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔𝑥) = 𝑧))
9087, 88, 89sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑔𝑥) = 𝑧)
9175, 83, 903eqtr3d 2662 . . . . . . . . . 10 (𝜏𝑦 = 𝑧)
9249, 91bnj593 30789 . . . . . . . . 9 (𝜃 → ∃𝑔 𝑦 = 𝑧)
9392bnj937 30816 . . . . . . . 8 (𝜃𝑦 = 𝑧)
9428, 93bnj593 30789 . . . . . . 7 (𝜒 → ∃𝑓 𝑦 = 𝑧)
9594bnj937 30816 . . . . . 6 (𝜒𝑦 = 𝑧)
9617, 95sylbir 225 . . . . 5 ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)
97963expib 1266 . . . 4 (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9897alrimivv 1854 . . 3 (𝜓 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9998alrimiv 1853 . 2 (𝜓 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
100 dffun4 5888 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)))
10116, 99, 100sylanbrc 697 1 (𝜓 → Fun 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036  wal 1479   = wceq 1481  wex 1702  wcel 1988  wral 2909  wrex 2910  cin 3566  cop 4174   cuni 4427  dom cdm 5104  cres 5106  Rel wrel 5109  Fun wfun 5870  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-res 5116  df-iota 5839  df-fun 5878  df-fv 5884
This theorem is referenced by:  bnj1383  30876
  Copyright terms: Public domain W3C validator