Metamath Proof Explorer


Theorem fsets

Description: The structure replacement function is a function. (Contributed by SO, 12-Jul-2018)

Ref Expression
Assertion fsets F V F : A B X A Y B F sSet X Y : A B

Proof

Step Hyp Ref Expression
1 difss A X A
2 fssres F : A B A X A F A X : A X B
3 1 2 mpan2 F : A B F A X : A X B
4 ffn F : A B F Fn A
5 fnresdm F Fn A F A = F
6 4 5 syl F : A B F A = F
7 6 reseq1d F : A B F A V X = F V X
8 resres F A V X = F A V X
9 invdif A V X = A X
10 9 reseq2i F A V X = F A X
11 8 10 eqtri F A V X = F A X
12 7 11 eqtr3di F : A B F V X = F A X
13 12 feq1d F : A B F V X : A X B F A X : A X B
14 3 13 mpbird F : A B F V X : A X B
15 14 adantl F V F : A B F V X : A X B
16 fsnunf2 F V X : A X B X A Y B F V X X Y : A B
17 15 16 syl3an1 F V F : A B X A Y B F V X X Y : A B
18 simp1l F V F : A B X A Y B F V
19 simp3 F V F : A B X A Y B Y B
20 setsval F V Y B F sSet X Y = F V X X Y
21 20 feq1d F V Y B F sSet X Y : A B F V X X Y : A B
22 18 19 21 syl2anc F V F : A B X A Y B F sSet X Y : A B F V X X Y : A B
23 17 22 mpbird F V F : A B X A Y B F sSet X Y : A B