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 34822
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 34773 . . . . . . 7 (𝜑 → ∀𝑓𝜑)
43nf5i 2143 . . . . . 6 𝑓𝜑
5 nfra1 3281 . . . . . 6 𝑓𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
64, 5nfan 1896 . . . . 5 𝑓(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
71, 6nfxfr 1849 . . . 4 𝑓𝜓
82bnj946 34766 . . . . . . . 8 (𝜑 ↔ ∀𝑓(𝑓𝐴 → Fun 𝑓))
98biimpi 216 . . . . . . 7 (𝜑 → ∀𝑓(𝑓𝐴 → Fun 𝑓))
10919.21bi 2186 . . . . . 6 (𝜑 → (𝑓𝐴 → Fun 𝑓))
111, 10bnj832 34750 . . . . 5 (𝜓 → (𝑓𝐴 → Fun 𝑓))
12 funrel 6584 . . . . 5 (Fun 𝑓 → Rel 𝑓)
1311, 12syl6 35 . . . 4 (𝜓 → (𝑓𝐴 → Rel 𝑓))
147, 13ralrimi 3254 . . 3 (𝜓 → ∀𝑓𝐴 Rel 𝑓)
15 reluni 5830 . . 3 (Rel 𝐴 ↔ ∀𝑓𝐴 Rel 𝑓)
1614, 15sylibr 234 . 2 (𝜓 → Rel 𝐴)
17 bnj1379.5 . . . . . 6 (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴))
18 eluni2 4915 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
1918biimpi 216 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
2019bnj1196 34786 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
2117, 20bnj836 34752 . . . . . . . . 9 (𝜒 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22 bnj1379.6 . . . . . . . . 9 (𝜃 ↔ (𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23 nfv 1911 . . . . . . . . . . . 12 𝑓𝑥, 𝑦⟩ ∈ 𝐴
24 nfv 1911 . . . . . . . . . . . 12 𝑓𝑥, 𝑧⟩ ∈ 𝐴
257, 23, 24nf3an 1898 . . . . . . . . . . 11 𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
2617, 25nfxfr 1849 . . . . . . . . . 10 𝑓𝜒
2726nf5ri 2192 . . . . . . . . 9 (𝜒 → ∀𝑓𝜒)
2821, 22, 27bnj1345 34816 . . . . . . . 8 (𝜒 → ∃𝑓𝜃)
2917simp3bi 1146 . . . . . . . . . . . . 13 (𝜒 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
3022, 29bnj835 34751 . . . . . . . . . . . 12 (𝜃 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
31 eluni2 4915 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑧⟩ ∈ 𝐴 ↔ ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3231biimpi 216 . . . . . . . . . . . . 13 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3332bnj1196 34786 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
3430, 33syl 17 . . . . . . . . . . 11 (𝜃 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35 bnj1379.7 . . . . . . . . . . 11 (𝜏 ↔ (𝜃𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36 nfv 1911 . . . . . . . . . . . . . . . . . 18 𝑔𝜑
37 nfra2w 3296 . . . . . . . . . . . . . . . . . 18 𝑔𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
3836, 37nfan 1896 . . . . . . . . . . . . . . . . 17 𝑔(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
391, 38nfxfr 1849 . . . . . . . . . . . . . . . 16 𝑔𝜓
40 nfv 1911 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑦⟩ ∈ 𝐴
41 nfv 1911 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑧⟩ ∈ 𝐴
4239, 40, 41nf3an 1898 . . . . . . . . . . . . . . 15 𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
4317, 42nfxfr 1849 . . . . . . . . . . . . . 14 𝑔𝜒
44 nfv 1911 . . . . . . . . . . . . . 14 𝑔 𝑓𝐴
45 nfv 1911 . . . . . . . . . . . . . 14 𝑔𝑥, 𝑦⟩ ∈ 𝑓
4643, 44, 45nf3an 1898 . . . . . . . . . . . . 13 𝑔(𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
4722, 46nfxfr 1849 . . . . . . . . . . . 12 𝑔𝜃
4847nf5ri 2192 . . . . . . . . . . 11 (𝜃 → ∀𝑔𝜃)
4934, 35, 48bnj1345 34816 . . . . . . . . . 10 (𝜃 → ∃𝑔𝜏)
501simprbi 496 . . . . . . . . . . . . . . . . . 18 (𝜓 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5117, 50bnj835 34751 . . . . . . . . . . . . . . . . 17 (𝜒 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5222, 51bnj835 34751 . . . . . . . . . . . . . . . 16 (𝜃 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5335, 52bnj835 34751 . . . . . . . . . . . . . . 15 (𝜏 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5422, 35bnj1219 34792 . . . . . . . . . . . . . . 15 (𝜏𝑓𝐴)
5553, 54bnj1294 34809 . . . . . . . . . . . . . 14 (𝜏 → ∀𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5635simp2bi 1145 . . . . . . . . . . . . . 14 (𝜏𝑔𝐴)
5755, 56bnj1294 34809 . . . . . . . . . . . . 13 (𝜏 → (𝑓𝐷) = (𝑔𝐷))
5857fveq1d 6908 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = ((𝑔𝐷)‘𝑥))
5922simp3bi 1146 . . . . . . . . . . . . . . . . 17 (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
6035, 59bnj835 34751 . . . . . . . . . . . . . . . 16 (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61 vex 3481 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
62 vex 3481 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
6361, 62opeldm 5920 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑓𝑥 ∈ dom 𝑓)
6460, 63syl 17 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑓)
65 vex 3481 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6661, 65opeldm 5920 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑧⟩ ∈ 𝑔𝑥 ∈ dom 𝑔)
6735, 66bnj837 34753 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑔)
6864, 67elind 4209 . . . . . . . . . . . . . 14 (𝜏𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69 bnj1379.2 . . . . . . . . . . . . . 14 𝐷 = (dom 𝑓 ∩ dom 𝑔)
7068, 69eleqtrrdi 2849 . . . . . . . . . . . . 13 (𝜏𝑥𝐷)
7170fvresd 6926 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = (𝑓𝑥))
7270fvresd 6926 . . . . . . . . . . . 12 (𝜏 → ((𝑔𝐷)‘𝑥) = (𝑔𝑥))
7358, 71, 723eqtr3d 2782 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = (𝑔𝑥))
742biimpi 216 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑓𝐴 Fun 𝑓)
751, 74bnj832 34750 . . . . . . . . . . . . . . . 16 (𝜓 → ∀𝑓𝐴 Fun 𝑓)
7617, 75bnj835 34751 . . . . . . . . . . . . . . 15 (𝜒 → ∀𝑓𝐴 Fun 𝑓)
7722, 76bnj835 34751 . . . . . . . . . . . . . 14 (𝜃 → ∀𝑓𝐴 Fun 𝑓)
7835, 77bnj835 34751 . . . . . . . . . . . . 13 (𝜏 → ∀𝑓𝐴 Fun 𝑓)
7978, 54bnj1294 34809 . . . . . . . . . . . 12 (𝜏 → Fun 𝑓)
80 funopfv 6958 . . . . . . . . . . . 12 (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓𝑥) = 𝑦))
8179, 60, 80sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = 𝑦)
82 funeq 6587 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
8382, 78, 56rspcdva 3622 . . . . . . . . . . . 12 (𝜏 → Fun 𝑔)
8435simp3bi 1146 . . . . . . . . . . . 12 (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
85 funopfv 6958 . . . . . . . . . . . 12 (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔𝑥) = 𝑧))
8683, 84, 85sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑔𝑥) = 𝑧)
8773, 81, 863eqtr3d 2782 . . . . . . . . . 10 (𝜏𝑦 = 𝑧)
8849, 87bnj593 34737 . . . . . . . . 9 (𝜃 → ∃𝑔 𝑦 = 𝑧)
8988bnj937 34763 . . . . . . . 8 (𝜃𝑦 = 𝑧)
9028, 89bnj593 34737 . . . . . . 7 (𝜒 → ∃𝑓 𝑦 = 𝑧)
9190bnj937 34763 . . . . . 6 (𝜒𝑦 = 𝑧)
9217, 91sylbir 235 . . . . 5 ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)
93923expib 1121 . . . 4 (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9493alrimivv 1925 . . 3 (𝜓 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9594alrimiv 1924 . 2 (𝜓 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
96 dffun4 6578 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)))
9716, 95, 96sylanbrc 583 1 (𝜓 → Fun 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086  wal 1534   = wceq 1536  wex 1775  wcel 2105  wral 3058  wrex 3067  cin 3961  cop 4636   cuni 4911  dom cdm 5688  cres 5690  Rel wrel 5693  Fun wfun 6556  cfv 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-res 5700  df-iota 6515  df-fun 6564  df-fv 6570
This theorem is referenced by:  bnj1383  34823
  Copyright terms: Public domain W3C validator