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 31027
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 30978 . . . . . . 7 (𝜑 → ∀𝑓𝜑)
43nf5i 2064 . . . . . 6 𝑓𝜑
5 nfra1 2970 . . . . . 6 𝑓𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
64, 5nfan 1868 . . . . 5 𝑓(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
71, 6nfxfr 1819 . . . 4 𝑓𝜓
82bnj946 30971 . . . . . . . 8 (𝜑 ↔ ∀𝑓(𝑓𝐴 → Fun 𝑓))
98biimpi 206 . . . . . . 7 (𝜑 → ∀𝑓(𝑓𝐴 → Fun 𝑓))
10919.21bi 2097 . . . . . 6 (𝜑 → (𝑓𝐴 → Fun 𝑓))
111, 10bnj832 30954 . . . . 5 (𝜓 → (𝑓𝐴 → Fun 𝑓))
12 funrel 5943 . . . . 5 (Fun 𝑓 → Rel 𝑓)
1311, 12syl6 35 . . . 4 (𝜓 → (𝑓𝐴 → Rel 𝑓))
147, 13ralrimi 2986 . . 3 (𝜓 → ∀𝑓𝐴 Rel 𝑓)
15 reluni 5274 . . 3 (Rel 𝐴 ↔ ∀𝑓𝐴 Rel 𝑓)
1614, 15sylibr 224 . 2 (𝜓 → Rel 𝐴)
17 bnj1379.5 . . . . . 6 (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴))
18 eluni2 4472 . . . . . . . . . . . 12 (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
1918biimpi 206 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓𝐴𝑥, 𝑦⟩ ∈ 𝑓)
2019bnj1196 30991 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
2117, 20bnj836 30956 . . . . . . . . 9 (𝜒 → ∃𝑓(𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
22 bnj1379.6 . . . . . . . . 9 (𝜃 ↔ (𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))
23 nfv 1883 . . . . . . . . . . . 12 𝑓𝑥, 𝑦⟩ ∈ 𝐴
24 nfv 1883 . . . . . . . . . . . 12 𝑓𝑥, 𝑧⟩ ∈ 𝐴
257, 23, 24nf3an 1871 . . . . . . . . . . 11 𝑓(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
2617, 25nfxfr 1819 . . . . . . . . . 10 𝑓𝜒
2726nf5ri 2103 . . . . . . . . 9 (𝜒 → ∀𝑓𝜒)
2821, 22, 27bnj1345 31021 . . . . . . . 8 (𝜒 → ∃𝑓𝜃)
2917simp3bi 1098 . . . . . . . . . . . . 13 (𝜒 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
3022, 29bnj835 30955 . . . . . . . . . . . 12 (𝜃 → ⟨𝑥, 𝑧⟩ ∈ 𝐴)
31 eluni2 4472 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑧⟩ ∈ 𝐴 ↔ ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3231biimpi 206 . . . . . . . . . . . . 13 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔𝐴𝑥, 𝑧⟩ ∈ 𝑔)
3332bnj1196 30991 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ 𝐴 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
3430, 33syl 17 . . . . . . . . . . 11 (𝜃 → ∃𝑔(𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
35 bnj1379.7 . . . . . . . . . . 11 (𝜏 ↔ (𝜃𝑔𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))
36 nfv 1883 . . . . . . . . . . . . . . . . . 18 𝑔𝜑
37 nfra2 2975 . . . . . . . . . . . . . . . . . 18 𝑔𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷)
3836, 37nfan 1868 . . . . . . . . . . . . . . . . 17 𝑔(𝜑 ∧ ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
391, 38nfxfr 1819 . . . . . . . . . . . . . . . 16 𝑔𝜓
40 nfv 1883 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑦⟩ ∈ 𝐴
41 nfv 1883 . . . . . . . . . . . . . . . 16 𝑔𝑥, 𝑧⟩ ∈ 𝐴
4239, 40, 41nf3an 1871 . . . . . . . . . . . . . . 15 𝑔(𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴)
4317, 42nfxfr 1819 . . . . . . . . . . . . . 14 𝑔𝜒
44 nfv 1883 . . . . . . . . . . . . . 14 𝑔 𝑓𝐴
45 nfv 1883 . . . . . . . . . . . . . 14 𝑔𝑥, 𝑦⟩ ∈ 𝑓
4643, 44, 45nf3an 1871 . . . . . . . . . . . . 13 𝑔(𝜒𝑓𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓)
4722, 46nfxfr 1819 . . . . . . . . . . . 12 𝑔𝜃
4847nf5ri 2103 . . . . . . . . . . 11 (𝜃 → ∀𝑔𝜃)
4934, 35, 48bnj1345 31021 . . . . . . . . . 10 (𝜃 → ∃𝑔𝜏)
501simprbi 479 . . . . . . . . . . . . . . . . . 18 (𝜓 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5117, 50bnj835 30955 . . . . . . . . . . . . . . . . 17 (𝜒 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5222, 51bnj835 30955 . . . . . . . . . . . . . . . 16 (𝜃 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5335, 52bnj835 30955 . . . . . . . . . . . . . . 15 (𝜏 → ∀𝑓𝐴𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5422, 35bnj1219 30997 . . . . . . . . . . . . . . 15 (𝜏𝑓𝐴)
5553, 54bnj1294 31014 . . . . . . . . . . . . . 14 (𝜏 → ∀𝑔𝐴 (𝑓𝐷) = (𝑔𝐷))
5635simp2bi 1097 . . . . . . . . . . . . . 14 (𝜏𝑔𝐴)
5755, 56bnj1294 31014 . . . . . . . . . . . . 13 (𝜏 → (𝑓𝐷) = (𝑔𝐷))
5857fveq1d 6231 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = ((𝑔𝐷)‘𝑥))
5922simp3bi 1098 . . . . . . . . . . . . . . . . 17 (𝜃 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
6035, 59bnj835 30955 . . . . . . . . . . . . . . . 16 (𝜏 → ⟨𝑥, 𝑦⟩ ∈ 𝑓)
61 vex 3234 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
62 vex 3234 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
6361, 62opeldm 5360 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑓𝑥 ∈ dom 𝑓)
6460, 63syl 17 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑓)
65 vex 3234 . . . . . . . . . . . . . . . . 17 𝑧 ∈ V
6661, 65opeldm 5360 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑧⟩ ∈ 𝑔𝑥 ∈ dom 𝑔)
6735, 66bnj837 30957 . . . . . . . . . . . . . . 15 (𝜏𝑥 ∈ dom 𝑔)
6864, 67elind 3831 . . . . . . . . . . . . . 14 (𝜏𝑥 ∈ (dom 𝑓 ∩ dom 𝑔))
69 bnj1379.2 . . . . . . . . . . . . . 14 𝐷 = (dom 𝑓 ∩ dom 𝑔)
7068, 69syl6eleqr 2741 . . . . . . . . . . . . 13 (𝜏𝑥𝐷)
71 fvres 6245 . . . . . . . . . . . . 13 (𝑥𝐷 → ((𝑓𝐷)‘𝑥) = (𝑓𝑥))
7270, 71syl 17 . . . . . . . . . . . 12 (𝜏 → ((𝑓𝐷)‘𝑥) = (𝑓𝑥))
73 fvres 6245 . . . . . . . . . . . . 13 (𝑥𝐷 → ((𝑔𝐷)‘𝑥) = (𝑔𝑥))
7470, 73syl 17 . . . . . . . . . . . 12 (𝜏 → ((𝑔𝐷)‘𝑥) = (𝑔𝑥))
7558, 72, 743eqtr3d 2693 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = (𝑔𝑥))
762biimpi 206 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑓𝐴 Fun 𝑓)
771, 76bnj832 30954 . . . . . . . . . . . . . . . 16 (𝜓 → ∀𝑓𝐴 Fun 𝑓)
7817, 77bnj835 30955 . . . . . . . . . . . . . . 15 (𝜒 → ∀𝑓𝐴 Fun 𝑓)
7922, 78bnj835 30955 . . . . . . . . . . . . . 14 (𝜃 → ∀𝑓𝐴 Fun 𝑓)
8035, 79bnj835 30955 . . . . . . . . . . . . 13 (𝜏 → ∀𝑓𝐴 Fun 𝑓)
8180, 54bnj1294 31014 . . . . . . . . . . . 12 (𝜏 → Fun 𝑓)
82 funopfv 6273 . . . . . . . . . . . 12 (Fun 𝑓 → (⟨𝑥, 𝑦⟩ ∈ 𝑓 → (𝑓𝑥) = 𝑦))
8381, 60, 82sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑓𝑥) = 𝑦)
84 funeq 5946 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
8584cbvralv 3201 . . . . . . . . . . . . . 14 (∀𝑓𝐴 Fun 𝑓 ↔ ∀𝑔𝐴 Fun 𝑔)
8680, 85sylib 208 . . . . . . . . . . . . 13 (𝜏 → ∀𝑔𝐴 Fun 𝑔)
8786, 56bnj1294 31014 . . . . . . . . . . . 12 (𝜏 → Fun 𝑔)
8835simp3bi 1098 . . . . . . . . . . . 12 (𝜏 → ⟨𝑥, 𝑧⟩ ∈ 𝑔)
89 funopfv 6273 . . . . . . . . . . . 12 (Fun 𝑔 → (⟨𝑥, 𝑧⟩ ∈ 𝑔 → (𝑔𝑥) = 𝑧))
9087, 88, 89sylc 65 . . . . . . . . . . 11 (𝜏 → (𝑔𝑥) = 𝑧)
9175, 83, 903eqtr3d 2693 . . . . . . . . . 10 (𝜏𝑦 = 𝑧)
9249, 91bnj593 30941 . . . . . . . . 9 (𝜃 → ∃𝑔 𝑦 = 𝑧)
9392bnj937 30968 . . . . . . . 8 (𝜃𝑦 = 𝑧)
9428, 93bnj593 30941 . . . . . . 7 (𝜒 → ∃𝑓 𝑦 = 𝑧)
9594bnj937 30968 . . . . . 6 (𝜒𝑦 = 𝑧)
9617, 95sylbir 225 . . . . 5 ((𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)
97963expib 1287 . . . 4 (𝜓 → ((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9897alrimivv 1896 . . 3 (𝜓 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
9998alrimiv 1895 . 2 (𝜓 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧))
100 dffun4 5938 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐴) → 𝑦 = 𝑧)))
10116, 99, 100sylanbrc 699 1 (𝜓 → Fun 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054  wal 1521   = wceq 1523  wex 1744  wcel 2030  wral 2941  wrex 2942  cin 3606  cop 4216   cuni 4468  dom cdm 5143  cres 5145  Rel wrel 5148  Fun wfun 5920  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-res 5155  df-iota 5889  df-fun 5928  df-fv 5934
This theorem is referenced by:  bnj1383  31028
  Copyright terms: Public domain W3C validator