Metamath Proof Explorer


Theorem mapfien2

Description: Equinumerousity relation for sets of finitely supported functions. (Contributed by Stefan O'Rear, 9-Jul-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses mapfien2.s S = x B A | finSupp 0 ˙ x
mapfien2.t T = x D C | finSupp W x
mapfien2.ac φ A C
mapfien2.bd φ B D
mapfien2.z φ 0 ˙ B
mapfien2.w φ W D
Assertion mapfien2 φ S T

Proof

Step Hyp Ref Expression
1 mapfien2.s S = x B A | finSupp 0 ˙ x
2 mapfien2.t T = x D C | finSupp W x
3 mapfien2.ac φ A C
4 mapfien2.bd φ B D
5 mapfien2.z φ 0 ˙ B
6 mapfien2.w φ W D
7 enfixsn 0 ˙ B W D B D y y : B 1-1 onto D y 0 ˙ = W
8 5 6 4 7 syl3anc φ y y : B 1-1 onto D y 0 ˙ = W
9 bren A C z z : A 1-1 onto C
10 3 9 sylib φ z z : A 1-1 onto C
11 eqid x D C | finSupp y 0 ˙ x = x D C | finSupp y 0 ˙ x
12 eqid y 0 ˙ = y 0 ˙
13 f1ocnv z : A 1-1 onto C z -1 : C 1-1 onto A
14 13 3ad2ant2 φ z : A 1-1 onto C y : B 1-1 onto D z -1 : C 1-1 onto A
15 simp3 φ z : A 1-1 onto C y : B 1-1 onto D y : B 1-1 onto D
16 3 3ad2ant1 φ z : A 1-1 onto C y : B 1-1 onto D A C
17 relen Rel
18 17 brrelex1i A C A V
19 16 18 syl φ z : A 1-1 onto C y : B 1-1 onto D A V
20 4 3ad2ant1 φ z : A 1-1 onto C y : B 1-1 onto D B D
21 17 brrelex1i B D B V
22 20 21 syl φ z : A 1-1 onto C y : B 1-1 onto D B V
23 17 brrelex2i A C C V
24 16 23 syl φ z : A 1-1 onto C y : B 1-1 onto D C V
25 17 brrelex2i B D D V
26 20 25 syl φ z : A 1-1 onto C y : B 1-1 onto D D V
27 5 3ad2ant1 φ z : A 1-1 onto C y : B 1-1 onto D 0 ˙ B
28 1 11 12 14 15 19 22 24 26 27 mapfien φ z : A 1-1 onto C y : B 1-1 onto D w S y w z -1 : S 1-1 onto x D C | finSupp y 0 ˙ x
29 ovex B A V
30 1 29 rabex2 S V
31 30 f1oen w S y w z -1 : S 1-1 onto x D C | finSupp y 0 ˙ x S x D C | finSupp y 0 ˙ x
32 28 31 syl φ z : A 1-1 onto C y : B 1-1 onto D S x D C | finSupp y 0 ˙ x
33 32 3adant3r φ z : A 1-1 onto C y : B 1-1 onto D y 0 ˙ = W S x D C | finSupp y 0 ˙ x
34 breq2 y 0 ˙ = W finSupp y 0 ˙ x finSupp W x
35 34 rabbidv y 0 ˙ = W x D C | finSupp y 0 ˙ x = x D C | finSupp W x
36 35 2 eqtr4di y 0 ˙ = W x D C | finSupp y 0 ˙ x = T
37 36 adantl y : B 1-1 onto D y 0 ˙ = W x D C | finSupp y 0 ˙ x = T
38 37 3ad2ant3 φ z : A 1-1 onto C y : B 1-1 onto D y 0 ˙ = W x D C | finSupp y 0 ˙ x = T
39 33 38 breqtrd φ z : A 1-1 onto C y : B 1-1 onto D y 0 ˙ = W S T
40 39 3exp φ z : A 1-1 onto C y : B 1-1 onto D y 0 ˙ = W S T
41 40 exlimdv φ z z : A 1-1 onto C y : B 1-1 onto D y 0 ˙ = W S T
42 10 41 mpd φ y : B 1-1 onto D y 0 ˙ = W S T
43 42 exlimdv φ y y : B 1-1 onto D y 0 ˙ = W S T
44 8 43 mpd φ S T