ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  funopg Structured version   GIF version

Theorem funopg 4856
Description: A Kuratowski ordered pair is a function only if its components are equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
funopg ((A 𝑉 B 𝑊 Fun ⟨A, B⟩) → A = B)

Proof of Theorem funopg
Dummy variables u 𝑡 v w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 3519 . . . . 5 (u = A → ⟨u, 𝑡⟩ = ⟨A, 𝑡⟩)
21funeqd 4845 . . . 4 (u = A → (Fun ⟨u, 𝑡⟩ ↔ Fun ⟨A, 𝑡⟩))
3 eqeq1 2024 . . . 4 (u = A → (u = 𝑡A = 𝑡))
42, 3imbi12d 223 . . 3 (u = A → ((Fun ⟨u, 𝑡⟩ → u = 𝑡) ↔ (Fun ⟨A, 𝑡⟩ → A = 𝑡)))
5 opeq2 3520 . . . . 5 (𝑡 = B → ⟨A, 𝑡⟩ = ⟨A, B⟩)
65funeqd 4845 . . . 4 (𝑡 = B → (Fun ⟨A, 𝑡⟩ ↔ Fun ⟨A, B⟩))
7 eqeq2 2027 . . . 4 (𝑡 = B → (A = 𝑡A = B))
86, 7imbi12d 223 . . 3 (𝑡 = B → ((Fun ⟨A, 𝑡⟩ → A = 𝑡) ↔ (Fun ⟨A, B⟩ → A = B)))
9 funrel 4841 . . . . 5 (Fun ⟨u, 𝑡⟩ → Rel ⟨u, 𝑡⟩)
10 vex 2534 . . . . . 6 u V
11 vex 2534 . . . . . 6 𝑡 V
1210, 11relop 4409 . . . . 5 (Rel ⟨u, 𝑡⟩ ↔ xy(u = {x} 𝑡 = {x, y}))
139, 12sylib 127 . . . 4 (Fun ⟨u, 𝑡⟩ → xy(u = {x} 𝑡 = {x, y}))
1410, 11opth 3944 . . . . . . . 8 (⟨u, 𝑡⟩ = ⟨{x}, {x, y}⟩ ↔ (u = {x} 𝑡 = {x, y}))
15 vex 2534 . . . . . . . . . . . 12 x V
1615opid 3537 . . . . . . . . . . 11 x, x⟩ = {{x}}
1716preq1i 3420 . . . . . . . . . 10 {⟨x, x⟩, {{x}, {x, y}}} = {{{x}}, {{x}, {x, y}}}
18 vex 2534 . . . . . . . . . . . 12 y V
1915, 18dfop 3518 . . . . . . . . . . 11 x, y⟩ = {{x}, {x, y}}
2019preq2i 3421 . . . . . . . . . 10 {⟨x, x⟩, ⟨x, y⟩} = {⟨x, x⟩, {{x}, {x, y}}}
21 snexgOLD 3905 . . . . . . . . . . . 12 (x V → {x} V)
2215, 21ax-mp 7 . . . . . . . . . . 11 {x} V
23 zfpair2 3915 . . . . . . . . . . 11 {x, y} V
2422, 23dfop 3518 . . . . . . . . . 10 ⟨{x}, {x, y}⟩ = {{{x}}, {{x}, {x, y}}}
2517, 20, 243eqtr4ri 2049 . . . . . . . . 9 ⟨{x}, {x, y}⟩ = {⟨x, x⟩, ⟨x, y⟩}
2625eqeq2i 2028 . . . . . . . 8 (⟨u, 𝑡⟩ = ⟨{x}, {x, y}⟩ ↔ ⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩})
2714, 26bitr3i 175 . . . . . . 7 ((u = {x} 𝑡 = {x, y}) ↔ ⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩})
28 dffun4 4836 . . . . . . . . 9 (Fun ⟨u, 𝑡⟩ ↔ (Rel ⟨u, 𝑡 zwv((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v)))
2928simprbi 260 . . . . . . . 8 (Fun ⟨u, 𝑡⟩ → zwv((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v))
3015, 15opex 3936 . . . . . . . . . . 11 x, x V
3130prid1 3446 . . . . . . . . . 10 x, x {⟨x, x⟩, ⟨x, y⟩}
32 eleq2 2079 . . . . . . . . . 10 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → (⟨x, xu, 𝑡⟩ ↔ ⟨x, x {⟨x, x⟩, ⟨x, y⟩}))
3331, 32mpbiri 157 . . . . . . . . 9 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → ⟨x, xu, 𝑡⟩)
3415, 18opex 3936 . . . . . . . . . . 11 x, y V
3534prid2 3447 . . . . . . . . . 10 x, y {⟨x, x⟩, ⟨x, y⟩}
36 eleq2 2079 . . . . . . . . . 10 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → (⟨x, yu, 𝑡⟩ ↔ ⟨x, y {⟨x, x⟩, ⟨x, y⟩}))
3735, 36mpbiri 157 . . . . . . . . 9 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → ⟨x, yu, 𝑡⟩)
3833, 37jca 290 . . . . . . . 8 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → (⟨x, xu, 𝑡x, yu, 𝑡⟩))
39 opeq12 3521 . . . . . . . . . . . . . 14 ((z = x w = x) → ⟨z, w⟩ = ⟨x, x⟩)
40393adant3 910 . . . . . . . . . . . . 13 ((z = x w = x v = y) → ⟨z, w⟩ = ⟨x, x⟩)
4140eleq1d 2084 . . . . . . . . . . . 12 ((z = x w = x v = y) → (⟨z, wu, 𝑡⟩ ↔ ⟨x, xu, 𝑡⟩))
42 opeq12 3521 . . . . . . . . . . . . . 14 ((z = x v = y) → ⟨z, v⟩ = ⟨x, y⟩)
43423adant2 909 . . . . . . . . . . . . 13 ((z = x w = x v = y) → ⟨z, v⟩ = ⟨x, y⟩)
4443eleq1d 2084 . . . . . . . . . . . 12 ((z = x w = x v = y) → (⟨z, vu, 𝑡⟩ ↔ ⟨x, yu, 𝑡⟩))
4541, 44anbi12d 445 . . . . . . . . . . 11 ((z = x w = x v = y) → ((⟨z, wu, 𝑡z, vu, 𝑡⟩) ↔ (⟨x, xu, 𝑡x, yu, 𝑡⟩)))
46 eqeq12 2030 . . . . . . . . . . . 12 ((w = x v = y) → (w = vx = y))
47463adant1 908 . . . . . . . . . . 11 ((z = x w = x v = y) → (w = vx = y))
4845, 47imbi12d 223 . . . . . . . . . 10 ((z = x w = x v = y) → (((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v) ↔ ((⟨x, xu, 𝑡x, yu, 𝑡⟩) → x = y)))
4948spc3gv 2618 . . . . . . . . 9 ((x V x V y V) → (zwv((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v) → ((⟨x, xu, 𝑡x, yu, 𝑡⟩) → x = y)))
5015, 15, 18, 49mp3an 1215 . . . . . . . 8 (zwv((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v) → ((⟨x, xu, 𝑡x, yu, 𝑡⟩) → x = y))
5129, 38, 50syl2im 34 . . . . . . 7 (Fun ⟨u, 𝑡⟩ → (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → x = y))
5227, 51syl5bi 141 . . . . . 6 (Fun ⟨u, 𝑡⟩ → ((u = {x} 𝑡 = {x, y}) → x = y))
53 dfsn2 3360 . . . . . . . . . . 11 {x} = {x, x}
54 preq2 3418 . . . . . . . . . . 11 (x = y → {x, x} = {x, y})
5553, 54syl5req 2063 . . . . . . . . . 10 (x = y → {x, y} = {x})
5655eqeq2d 2029 . . . . . . . . 9 (x = y → (𝑡 = {x, y} ↔ 𝑡 = {x}))
57 eqtr3 2037 . . . . . . . . . 10 ((u = {x} 𝑡 = {x}) → u = 𝑡)
5857expcom 109 . . . . . . . . 9 (𝑡 = {x} → (u = {x} → u = 𝑡))
5956, 58syl6bi 152 . . . . . . . 8 (x = y → (𝑡 = {x, y} → (u = {x} → u = 𝑡)))
6059com13 74 . . . . . . 7 (u = {x} → (𝑡 = {x, y} → (x = yu = 𝑡)))
6160imp 115 . . . . . 6 ((u = {x} 𝑡 = {x, y}) → (x = yu = 𝑡))
6252, 61sylcom 25 . . . . 5 (Fun ⟨u, 𝑡⟩ → ((u = {x} 𝑡 = {x, y}) → u = 𝑡))
6362exlimdvv 1755 . . . 4 (Fun ⟨u, 𝑡⟩ → (xy(u = {x} 𝑡 = {x, y}) → u = 𝑡))
6413, 63mpd 13 . . 3 (Fun ⟨u, 𝑡⟩ → u = 𝑡)
654, 8, 64vtocl2g 2590 . 2 ((A 𝑉 B 𝑊) → (Fun ⟨A, B⟩ → A = B))
66653impia 1085 1 ((A 𝑉 B 𝑊 Fun ⟨A, B⟩) → A = B)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 871  wal 1224   = wceq 1226  wex 1358   wcel 1370  Vcvv 2531  {csn 3346  {cpr 3347  cop 3349  Rel wrel 4273  Fun wfun 4819
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-br 3735  df-opab 3789  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-fun 4827
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator