Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fliftfun Unicode version

Theorem fliftfun 5697
 Description: The function is the unique function defined by , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
Hypotheses
Ref Expression
flift.1
flift.2
flift.3
fliftfun.4
fliftfun.5
Assertion
Ref Expression
fliftfun
Distinct variable groups:   ,   ,   ,   ,,   ,   ,   ,,   ,,   ,,
Allowed substitution hints:   ()   ()   ()   ()   ()

Proof of Theorem fliftfun
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1508 . . 3
2 flift.1 . . . . 5
3 nfmpt1 4021 . . . . . 6
43nfrn 4784 . . . . 5
52, 4nfcxfr 2278 . . . 4
65nffun 5146 . . 3
7 fveq2 5421 . . . . . . 7
8 simplr 519 . . . . . . . . 9
9 flift.2 . . . . . . . . . . 11
10 flift.3 . . . . . . . . . . 11
112, 9, 10fliftel1 5695 . . . . . . . . . 10
1211ad2ant2r 500 . . . . . . . . 9
13 funbrfv 5460 . . . . . . . . 9
148, 12, 13sylc 62 . . . . . . . 8
15 simprr 521 . . . . . . . . . . 11
16 eqidd 2140 . . . . . . . . . . 11
17 eqidd 2140 . . . . . . . . . . 11
18 fliftfun.4 . . . . . . . . . . . . . 14
1918eqeq2d 2151 . . . . . . . . . . . . 13
20 fliftfun.5 . . . . . . . . . . . . . 14
2120eqeq2d 2151 . . . . . . . . . . . . 13
2219, 21anbi12d 464 . . . . . . . . . . . 12
2322rspcev 2789 . . . . . . . . . . 11
2415, 16, 17, 23syl12anc 1214 . . . . . . . . . 10
252, 9, 10fliftel 5694 . . . . . . . . . . 11
2625ad2antrr 479 . . . . . . . . . 10
2724, 26mpbird 166 . . . . . . . . 9
28 funbrfv 5460 . . . . . . . . 9
298, 27, 28sylc 62 . . . . . . . 8
3014, 29eqeq12d 2154 . . . . . . 7
317, 30syl5ib 153 . . . . . 6
3231anassrs 397 . . . . 5
3332ralrimiva 2505 . . . 4
3433exp31 361 . . 3
351, 6, 34ralrimd 2510 . 2
362, 9, 10fliftel 5694 . . . . . . . . 9
372, 9, 10fliftel 5694 . . . . . . . . . 10
3818eqeq2d 2151 . . . . . . . . . . . 12
3920eqeq2d 2151 . . . . . . . . . . . 12
4038, 39anbi12d 464 . . . . . . . . . . 11
4140cbvrexv 2655 . . . . . . . . . 10
4237, 41syl6bb 195 . . . . . . . . 9
4336, 42anbi12d 464 . . . . . . . 8
4443biimpd 143 . . . . . . 7
45 reeanv 2600 . . . . . . . 8
46 r19.29 2569 . . . . . . . . . 10
47 r19.29 2569 . . . . . . . . . . . 12
48 eqtr2 2158 . . . . . . . . . . . . . . . . 17
4948ad2ant2r 500 . . . . . . . . . . . . . . . 16
5049imim1i 60 . . . . . . . . . . . . . . 15
5150imp 123 . . . . . . . . . . . . . 14
52 simprlr 527 . . . . . . . . . . . . . 14
53 simprrr 529 . . . . . . . . . . . . . 14
5451, 52, 533eqtr4d 2182 . . . . . . . . . . . . 13
5554rexlimivw 2545 . . . . . . . . . . . 12
5647, 55syl 14 . . . . . . . . . . 11
5756rexlimivw 2545 . . . . . . . . . 10
5846, 57syl 14 . . . . . . . . 9
5958ex 114 . . . . . . . 8
6045, 59syl5bir 152 . . . . . . 7
6144, 60syl9 72 . . . . . 6
6261alrimdv 1848 . . . . 5
6362alrimdv 1848 . . . 4
6463alrimdv 1848 . . 3
652, 9, 10fliftrel 5693 . . . . 5
66 relxp 4648 . . . . 5
67 relss 4626 . . . . 5
6865, 66, 67mpisyl 1422 . . . 4
69 dffun2 5133 . . . . 5
7069baib 904 . . . 4
7168, 70syl 14 . . 3
7264, 71sylibrd 168 . 2
7335, 72impbid 128 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104  wal 1329   wceq 1331   wcel 1480  wral 2416  wrex 2417   wss 3071  cop 3530   class class class wbr 3929   cmpt 3989   cxp 4537   crn 4540   wrel 4544   wfun 5117  cfv 5123 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-fv 5131 This theorem is referenced by:  fliftfund  5698  fliftfuns  5699  qliftfun  6511
 Copyright terms: Public domain W3C validator