Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsnunfv Structured version   Unicode version

Theorem fsnunfv 5934
 Description: Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.)
Assertion
Ref Expression
fsnunfv

Proof of Theorem fsnunfv
StepHypRef Expression
1 dmres 5168 . . . . . . . . 9
2 incom 3534 . . . . . . . . 9
31, 2eqtri 2457 . . . . . . . 8
4 disjsn 3869 . . . . . . . . 9
54biimpri 199 . . . . . . . 8
63, 5syl5eq 2481 . . . . . . 7
763ad2ant3 981 . . . . . 6
8 relres 5175 . . . . . . 7
9 reldm0 5088 . . . . . . 7
108, 9ax-mp 8 . . . . . 6
117, 10sylibr 205 . . . . 5
12 fnsng 5499 . . . . . . 7
13123adant3 978 . . . . . 6
14 fnresdm 5555 . . . . . 6
1513, 14syl 16 . . . . 5
1611, 15uneq12d 3503 . . . 4
17 resundir 5162 . . . 4
18 uncom 3492 . . . . 5
19 un0 3653 . . . . 5
2018, 19eqtr2i 2458 . . . 4
2116, 17, 203eqtr4g 2494 . . 3
2221fveq1d 5731 . 2
23 snidg 3840 . . . 4