Metamath Proof Explorer


Theorem pw2f1o2val2

Description: Membership in a mapped set under the pw2f1o2 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypothesis pw2f1o2.f F = x 2 𝑜 A x -1 1 𝑜
Assertion pw2f1o2val2 X 2 𝑜 A Y A Y F X X Y = 1 𝑜

Proof

Step Hyp Ref Expression
1 pw2f1o2.f F = x 2 𝑜 A x -1 1 𝑜
2 1 pw2f1o2val X 2 𝑜 A F X = X -1 1 𝑜
3 2 eleq2d X 2 𝑜 A Y F X Y X -1 1 𝑜
4 3 adantr X 2 𝑜 A Y A Y F X Y X -1 1 𝑜
5 elmapi X 2 𝑜 A X : A 2 𝑜
6 ffn X : A 2 𝑜 X Fn A
7 fniniseg X Fn A Y X -1 1 𝑜 Y A X Y = 1 𝑜
8 5 6 7 3syl X 2 𝑜 A Y X -1 1 𝑜 Y A X Y = 1 𝑜
9 8 baibd X 2 𝑜 A Y A Y X -1 1 𝑜 X Y = 1 𝑜
10 4 9 bitrd X 2 𝑜 A Y A Y F X X Y = 1 𝑜