Metamath Proof Explorer


Theorem en1OLD

Description: Obsolete version of en1 as of 23-Sep-2024. (Contributed by NM, 25-Jul-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en1OLD A 1 𝑜 x A = x

Proof

Step Hyp Ref Expression
1 df1o2 1 𝑜 =
2 1 breq2i A 1 𝑜 A
3 bren A f f : A 1-1 onto
4 2 3 bitri A 1 𝑜 f f : A 1-1 onto
5 f1ocnv f : A 1-1 onto f -1 : 1-1 onto A
6 f1ofo f -1 : 1-1 onto A f -1 : onto A
7 forn f -1 : onto A ran f -1 = A
8 6 7 syl f -1 : 1-1 onto A ran f -1 = A
9 f1of f -1 : 1-1 onto A f -1 : A
10 0ex V
11 10 fsn2 f -1 : A f -1 A f -1 = f -1
12 11 simprbi f -1 : A f -1 = f -1
13 9 12 syl f -1 : 1-1 onto A f -1 = f -1
14 13 rneqd f -1 : 1-1 onto A ran f -1 = ran f -1
15 10 rnsnop ran f -1 = f -1
16 14 15 eqtrdi f -1 : 1-1 onto A ran f -1 = f -1
17 8 16 eqtr3d f -1 : 1-1 onto A A = f -1
18 fvex f -1 V
19 sneq x = f -1 x = f -1
20 19 eqeq2d x = f -1 A = x A = f -1
21 18 20 spcev A = f -1 x A = x
22 5 17 21 3syl f : A 1-1 onto x A = x
23 22 exlimiv f f : A 1-1 onto x A = x
24 4 23 sylbi A 1 𝑜 x A = x
25 vex x V
26 25 ensn1 x 1 𝑜
27 breq1 A = x A 1 𝑜 x 1 𝑜
28 26 27 mpbiri A = x A 1 𝑜
29 28 exlimiv x A = x A 1 𝑜
30 24 29 impbii A 1 𝑜 x A = x