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

Theorem funopg 4877
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 3540 . . . . 5 (u = A → ⟨u, 𝑡⟩ = ⟨A, 𝑡⟩)
21funeqd 4866 . . . 4 (u = A → (Fun ⟨u, 𝑡⟩ ↔ Fun ⟨A, 𝑡⟩))
3 eqeq1 2043 . . . 4 (u = A → (u = 𝑡A = 𝑡))
42, 3imbi12d 223 . . 3 (u = A → ((Fun ⟨u, 𝑡⟩ → u = 𝑡) ↔ (Fun ⟨A, 𝑡⟩ → A = 𝑡)))
5 opeq2 3541 . . . . 5 (𝑡 = B → ⟨A, 𝑡⟩ = ⟨A, B⟩)
65funeqd 4866 . . . 4 (𝑡 = B → (Fun ⟨A, 𝑡⟩ ↔ Fun ⟨A, B⟩))
7 eqeq2 2046 . . . 4 (𝑡 = B → (A = 𝑡A = B))
86, 7imbi12d 223 . . 3 (𝑡 = B → ((Fun ⟨A, 𝑡⟩ → A = 𝑡) ↔ (Fun ⟨A, B⟩ → A = B)))
9 funrel 4862 . . . . 5 (Fun ⟨u, 𝑡⟩ → Rel ⟨u, 𝑡⟩)
10 vex 2554 . . . . . 6 u V
11 vex 2554 . . . . . 6 𝑡 V
1210, 11relop 4429 . . . . 5 (Rel ⟨u, 𝑡⟩ ↔ xy(u = {x} 𝑡 = {x, y}))
139, 12sylib 127 . . . 4 (Fun ⟨u, 𝑡⟩ → xy(u = {x} 𝑡 = {x, y}))
1410, 11opth 3965 . . . . . . . 8 (⟨u, 𝑡⟩ = ⟨{x}, {x, y}⟩ ↔ (u = {x} 𝑡 = {x, y}))
15 vex 2554 . . . . . . . . . . . 12 x V
1615opid 3558 . . . . . . . . . . 11 x, x⟩ = {{x}}
1716preq1i 3441 . . . . . . . . . 10 {⟨x, x⟩, {{x}, {x, y}}} = {{{x}}, {{x}, {x, y}}}
18 vex 2554 . . . . . . . . . . . 12 y V
1915, 18dfop 3539 . . . . . . . . . . 11 x, y⟩ = {{x}, {x, y}}
2019preq2i 3442 . . . . . . . . . 10 {⟨x, x⟩, ⟨x, y⟩} = {⟨x, x⟩, {{x}, {x, y}}}
21 snexgOLD 3926 . . . . . . . . . . . 12 (x V → {x} V)
2215, 21ax-mp 7 . . . . . . . . . . 11 {x} V
23 zfpair2 3936 . . . . . . . . . . 11 {x, y} V
2422, 23dfop 3539 . . . . . . . . . 10 ⟨{x}, {x, y}⟩ = {{{x}}, {{x}, {x, y}}}
2517, 20, 243eqtr4ri 2068 . . . . . . . . 9 ⟨{x}, {x, y}⟩ = {⟨x, x⟩, ⟨x, y⟩}
2625eqeq2i 2047 . . . . . . . 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 4856 . . . . . . . . 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 3957 . . . . . . . . . . 11 x, x V
3130prid1 3467 . . . . . . . . . 10 x, x {⟨x, x⟩, ⟨x, y⟩}
32 eleq2 2098 . . . . . . . . . 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 3957 . . . . . . . . . . 11 x, y V
3534prid2 3468 . . . . . . . . . 10 x, y {⟨x, x⟩, ⟨x, y⟩}
36 eleq2 2098 . . . . . . . . . 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 3542 . . . . . . . . . . . . . 14 ((z = x w = x) → ⟨z, w⟩ = ⟨x, x⟩)
40393adant3 923 . . . . . . . . . . . . 13 ((z = x w = x v = y) → ⟨z, w⟩ = ⟨x, x⟩)
4140eleq1d 2103 . . . . . . . . . . . 12 ((z = x w = x v = y) → (⟨z, wu, 𝑡⟩ ↔ ⟨x, xu, 𝑡⟩))
42 opeq12 3542 . . . . . . . . . . . . . 14 ((z = x v = y) → ⟨z, v⟩ = ⟨x, y⟩)
43423adant2 922 . . . . . . . . . . . . 13 ((z = x w = x v = y) → ⟨z, v⟩ = ⟨x, y⟩)
4443eleq1d 2103 . . . . . . . . . . . 12 ((z = x w = x v = y) → (⟨z, vu, 𝑡⟩ ↔ ⟨x, yu, 𝑡⟩))
4541, 44anbi12d 442 . . . . . . . . . . 11 ((z = x w = x v = y) → ((⟨z, wu, 𝑡z, vu, 𝑡⟩) ↔ (⟨x, xu, 𝑡x, yu, 𝑡⟩)))
46 eqeq12 2049 . . . . . . . . . . . 12 ((w = x v = y) → (w = vx = y))
47463adant1 921 . . . . . . . . . . 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 2639 . . . . . . . . 9 ((x V x V y V) → (zwv((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v) → ((⟨x, xu, 𝑡x, yu, 𝑡⟩) → x = y)))
5015, 15, 18, 49mp3an 1231 . . . . . . . 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 3381 . . . . . . . . . . 11 {x} = {x, x}
54 preq2 3439 . . . . . . . . . . 11 (x = y → {x, x} = {x, y})
5553, 54syl5req 2082 . . . . . . . . . 10 (x = y → {x, y} = {x})
5655eqeq2d 2048 . . . . . . . . 9 (x = y → (𝑡 = {x, y} ↔ 𝑡 = {x}))
57 eqtr3 2056 . . . . . . . . . 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 1774 . . . 4 (Fun ⟨u, 𝑡⟩ → (xy(u = {x} 𝑡 = {x, y}) → u = 𝑡))
6413, 63mpd 13 . . 3 (Fun ⟨u, 𝑡⟩ → u = 𝑡)
654, 8, 64vtocl2g 2611 . 2 ((A 𝑉 B 𝑊) → (Fun ⟨A, B⟩ → A = B))
66653impia 1100 1 ((A 𝑉 B 𝑊 Fun ⟨A, B⟩) → A = B)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 884  wal 1240   = wceq 1242  wex 1378   wcel 1390  Vcvv 2551  {csn 3367  {cpr 3368  cop 3370  Rel wrel 4293  Fun wfun 4839
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-fun 4847
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator