| Intuitionistic Logic Explorer | 
      
      
      < Previous  
      Next >
      
       Nearby theorems  | 
  ||
| Mirrors > Home > ILE Home > Th. List > fnpr2ob | Unicode version | ||
| Description: Biconditional version of fnpr2o 12982. (Contributed by Jim Kingdon, 27-Sep-2023.) | 
| Ref | Expression | 
|---|---|
| fnpr2ob | 
 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | fnpr2o 12982 | 
. 2
 | |
| 2 | 0ex 4160 | 
. . . . . . . 8
 | |
| 3 | 2 | prid1 3728 | 
. . . . . . 7
 | 
| 4 | df2o3 6488 | 
. . . . . . 7
 | |
| 5 | 3, 4 | eleqtrri 2272 | 
. . . . . 6
 | 
| 6 | fndm 5357 | 
. . . . . 6
 | |
| 7 | 5, 6 | eleqtrrid 2286 | 
. . . . 5
 | 
| 8 | 2 | eldm2 4864 | 
. . . . 5
 | 
| 9 | 7, 8 | sylib 122 | 
. . . 4
 | 
| 10 | 1n0 6490 | 
. . . . . . . . . . 11
 | |
| 11 | 10 | nesymi 2413 | 
. . . . . . . . . 10
 | 
| 12 | vex 2766 | 
. . . . . . . . . . 11
 | |
| 13 | 2, 12 | opth1 4269 | 
. . . . . . . . . 10
 | 
| 14 | 11, 13 | mto 663 | 
. . . . . . . . 9
 | 
| 15 | elpri 3645 | 
. . . . . . . . 9
 | |
| 16 | orel2 727 | 
. . . . . . . . 9
 | |
| 17 | 14, 15, 16 | mpsyl 65 | 
. . . . . . . 8
 | 
| 18 | 2, 12 | opth 4270 | 
. . . . . . . 8
 | 
| 19 | 17, 18 | sylib 122 | 
. . . . . . 7
 | 
| 20 | 19 | simprd 114 | 
. . . . . 6
 | 
| 21 | 20 | eximi 1614 | 
. . . . 5
 | 
| 22 | isset 2769 | 
. . . . 5
 | |
| 23 | 21, 22 | sylibr 134 | 
. . . 4
 | 
| 24 | 9, 23 | syl 14 | 
. . 3
 | 
| 25 | 1oex 6482 | 
. . . . . . . 8
 | |
| 26 | 25 | prid2 3729 | 
. . . . . . 7
 | 
| 27 | 26, 4 | eleqtrri 2272 | 
. . . . . 6
 | 
| 28 | 27, 6 | eleqtrrid 2286 | 
. . . . 5
 | 
| 29 | 25 | eldm2 4864 | 
. . . . 5
 | 
| 30 | 28, 29 | sylib 122 | 
. . . 4
 | 
| 31 | 10 | neii 2369 | 
. . . . . . . . . 10
 | 
| 32 | 25, 12 | opth1 4269 | 
. . . . . . . . . 10
 | 
| 33 | 31, 32 | mto 663 | 
. . . . . . . . 9
 | 
| 34 | elpri 3645 | 
. . . . . . . . . 10
 | |
| 35 | 34 | orcomd 730 | 
. . . . . . . . 9
 | 
| 36 | orel2 727 | 
. . . . . . . . 9
 | |
| 37 | 33, 35, 36 | mpsyl 65 | 
. . . . . . . 8
 | 
| 38 | 25, 12 | opth 4270 | 
. . . . . . . 8
 | 
| 39 | 37, 38 | sylib 122 | 
. . . . . . 7
 | 
| 40 | 39 | simprd 114 | 
. . . . . 6
 | 
| 41 | 40 | eximi 1614 | 
. . . . 5
 | 
| 42 | isset 2769 | 
. . . . 5
 | |
| 43 | 41, 42 | sylibr 134 | 
. . . 4
 | 
| 44 | 30, 43 | syl 14 | 
. . 3
 | 
| 45 | 24, 44 | jca 306 | 
. 2
 | 
| 46 | 1, 45 | impbii 126 | 
1
 | 
| Colors of variables: wff set class | 
| Syntax hints:    | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 | 
| This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-ral 2480 df-rex 2481 df-v 2765 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-br 4034 df-opab 4095 df-tr 4132 df-id 4328 df-iord 4401 df-on 4403 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-fun 5260 df-fn 5261 df-1o 6474 df-2o 6475 | 
| This theorem is referenced by: xpsfrnel2 12989 | 
| Copyright terms: Public domain | W3C validator |