Substitutions for these variable pairs may not have variables in common: (Dummy variables for use in proof:) x,y x,z x,w x,f x,A y,z y,w y,f y,A z,w z,f z,A w,f w,A A,f

Proof of Theorem canth2
  Step   Hyp     Ref     Expression
1               visset 1118     |- zV
2       1       snelpw 1471     |- (zA  {z}A)
3       2       biimp 118       |- (zA  {z}A)
4       3       rgen 1044       |- "zA{z}A
5               cleqid 940      |- {z , w|(zA  w = {z})} = {z , w|(zA  w = {z})}
6       5       fopab2 2111     |- ("zA{z}A  {z , w|(zA  w = {z})}:A*A)
7       4,6     ax-mp 6 |- {z , w|(zA  w = {z})}:A*A
8               sneq 1436       |- (z = x  {z} = {x})
9               snex 1470       |- {x}V
10      8,5,9   opabval2 2179   |- (xA  ({z , w|(zA  w = {z})}x) = {x})
11              sneq 1436       |- (z = y  {z} = {y})
12              snex 1470       |- {y}V
13      11,5,12 opabval2 2179   |- (yA  ({z , w|(zA  w = {z})}y) = {y})
14      10,13   cleqan12d 954   |- ((xA  yA)  (({z , w|(zA  w = {z})}x) = ({z , w|(zA  w = {z})}y)  {x} = {y}))
15              visset 1118     |- xV
16      15      sneqr 1468      |- ({x} = {y}  x = y)
17      14,16   syl6bi 172      |- ((xA  yA)  (({z , w|(zA  w = {z})}x) = ({z , w|(zA  w = {z})}y)  x = y))
18      17      rgen2 1045      |- "xA"yA(({z , w|(zA  w = {z})}x) = ({z , w|(zA  w = {z})}y)  x = y)
19      7,18    pm3.2i 211      |- ({z , w|(zA  w = {z})}:A*A  "xA"yA(({z , w|(zA  w = {z})}x) = ({z , w|(zA  w = {z})}y)  x = y))
20              f1fv 2198       |- ({z , w|(zA  w = {z})}:A*1-1A  ({z , w|(zA  w = {z})}:A*A  "xA"yA(({z , w|(zA  w = {z})}x) = ({z , w|(zA  w = {z})}y)  x = y)))
21      19,20   mpbir 150       |- {z , w|(zA  w = {z})}:A*1-1A
22              canth2.1        |- AV
23      22      f1dom 2446      |- ({z , w|(zA  w = {z})}:A*1-1A  AA)
24      21,23   ax-mp 6 |- AA
25      22      canth 2203      |- f:A*ontoA
26      25      nex 666 |- $ff:A*ontoA
27      22      zfpowcl 1427    |- AV
28      27      bren 2431       |- (AA  $ff:A*1-1-ontoA)
29              df-f1o 1897     |- (f:A*1-1-ontoA  (f:A*1-1A  f:A*ontoA))
30      29      pm3.27bd 240    |- (f:A*1-1-ontoA  f:A*ontoA)
31      30      19.22i 610      |- ($ff:A*1-1-ontoA  $ff:A*ontoA)
32      28,31   sylbi 159       |- (AA  $ff:A*ontoA)
33      32      con3 79 |- ($ff:A*ontoA  AA)
34      26,33   ax-mp 6 |- AA
35      24,34   pm3.2i 211      |- (AA  AA)
36              brsdom 2434     |- (A<A  (AA  AA))
37      35,36   mpbir 150       |- A<A
Syntax hints: wn  wi  wa  wex $ weq = cv [set] wceq = wcel  wral " cpw  csn { wbr [rel] copab { wf * wf1 *1-1 wfo *onto wf1o *1-1-onto cfv  cen  cdom  csdm < 
The theorem was proved from these axioms: ax-1 ax-2 ax-3 ax-mp ax-4 ax-5 ax-6 ax-7 ax-gen ax-8 ax-9 ax-10 ax-11 ax-12 ax-14 ax-16 ax-17 ax-ext ax-rep ax-un ax-pow 
Colors of variables: wff set class