Metamath Proof Explorer


Theorem f1oweALT

Description: Alternate proof of f1owe , more direct since not using the isomorphism predicate, but requiring ax-un . (Contributed by NM, 4-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis f1oweALT.1 R = x y | F x S F y
Assertion f1oweALT F : A 1-1 onto B S We B R We A

Proof

Step Hyp Ref Expression
1 f1oweALT.1 R = x y | F x S F y
2 f1ofo F : A 1-1 onto B F : A onto B
3 df-fo F : A onto B F Fn A ran F = B
4 freq2 ran F = B S Fr ran F S Fr B
5 4 biimprd ran F = B S Fr B S Fr ran F
6 df-fn F Fn A Fun F dom F = A
7 df-fr S Fr ran F w w ran F w u w f w ¬ f S u
8 vex z V
9 8 funimaex Fun F F z V
10 n0 z w w z
11 funfvima2 Fun F z dom F w z F w F z
12 ne0i F w F z F z
13 11 12 syl6 Fun F z dom F w z F z
14 13 exlimdv Fun F z dom F w w z F z
15 10 14 syl5bi Fun F z dom F z F z
16 15 imp Fun F z dom F z F z
17 imassrn F z ran F
18 16 17 jctil Fun F z dom F z F z ran F F z
19 sseq1 w = F z w ran F F z ran F
20 neeq1 w = F z w F z
21 19 20 anbi12d w = F z w ran F w F z ran F F z
22 raleq w = F z f w ¬ f S u f F z ¬ f S u
23 22 rexeqbi1dv w = F z u w f w ¬ f S u u F z f F z ¬ f S u
24 21 23 imbi12d w = F z w ran F w u w f w ¬ f S u F z ran F F z u F z f F z ¬ f S u
25 24 spcgv F z V w w ran F w u w f w ¬ f S u F z ran F F z u F z f F z ¬ f S u
26 18 25 syl7 F z V w w ran F w u w f w ¬ f S u Fun F z dom F z u F z f F z ¬ f S u
27 9 26 syl Fun F w w ran F w u w f w ¬ f S u Fun F z dom F z u F z f F z ¬ f S u
28 7 27 syl5bi Fun F S Fr ran F Fun F z dom F z u F z f F z ¬ f S u
29 28 com23 Fun F Fun F z dom F z S Fr ran F u F z f F z ¬ f S u
30 29 expd Fun F Fun F z dom F z S Fr ran F u F z f F z ¬ f S u
31 30 anabsi5 Fun F z dom F z S Fr ran F u F z f F z ¬ f S u
32 31 impd Fun F z dom F z S Fr ran F u F z f F z ¬ f S u
33 fores Fun F z dom F F z : z onto F z
34 vex v V
35 vex w V
36 fveq2 x = v F x = F v
37 36 breq1d x = v F x S F y F v S F y
38 fveq2 y = w F y = F w
39 38 breq2d y = w F v S F y F v S F w
40 34 35 37 39 1 brab v R w F v S F w
41 fvres v z F z v = F v
42 fvres w z F z w = F w
43 41 42 breqan12rd w z v z F z v S F z w F v S F w
44 40 43 bitr4id w z v z v R w F z v S F z w
45 44 notbid w z v z ¬ v R w ¬ F z v S F z w
46 45 ralbidva w z v z ¬ v R w v z ¬ F z v S F z w
47 46 rexbiia w z v z ¬ v R w w z v z ¬ F z v S F z w
48 breq1 F z v = f F z v S F z w f S F z w
49 48 notbid F z v = f ¬ F z v S F z w ¬ f S F z w
50 49 cbvfo F z : z onto F z v z ¬ F z v S F z w f F z ¬ f S F z w
51 50 rexbidv F z : z onto F z w z v z ¬ F z v S F z w w z f F z ¬ f S F z w
52 breq2 F z w = u f S F z w f S u
53 52 notbid F z w = u ¬ f S F z w ¬ f S u
54 53 ralbidv F z w = u f F z ¬ f S F z w f F z ¬ f S u
55 54 cbvexfo F z : z onto F z w z f F z ¬ f S F z w u F z f F z ¬ f S u
56 51 55 bitrd F z : z onto F z w z v z ¬ F z v S F z w u F z f F z ¬ f S u
57 47 56 syl5bb F z : z onto F z w z v z ¬ v R w u F z f F z ¬ f S u
58 33 57 syl Fun F z dom F w z v z ¬ v R w u F z f F z ¬ f S u
59 32 58 sylibrd Fun F z dom F z S Fr ran F w z v z ¬ v R w
60 59 exp4b Fun F z dom F z S Fr ran F w z v z ¬ v R w
61 60 com34 Fun F z dom F S Fr ran F z w z v z ¬ v R w
62 61 com23 Fun F S Fr ran F z dom F z w z v z ¬ v R w
63 62 imp4a Fun F S Fr ran F z dom F z w z v z ¬ v R w
64 63 alrimdv Fun F S Fr ran F z z dom F z w z v z ¬ v R w
65 df-fr R Fr dom F z z dom F z w z v z ¬ v R w
66 64 65 syl6ibr Fun F S Fr ran F R Fr dom F
67 freq2 dom F = A R Fr dom F R Fr A
68 67 biimpd dom F = A R Fr dom F R Fr A
69 66 68 sylan9 Fun F dom F = A S Fr ran F R Fr A
70 6 69 sylbi F Fn A S Fr ran F R Fr A
71 5 70 sylan9r F Fn A ran F = B S Fr B R Fr A
72 3 71 sylbi F : A onto B S Fr B R Fr A
73 2 72 syl F : A 1-1 onto B S Fr B R Fr A
74 df-f1o F : A 1-1 onto B F : A 1-1 B F : A onto B
75 fveq2 x = w F x = F w
76 75 breq1d x = w F x S F y F w S F y
77 fveq2 y = v F y = F v
78 77 breq2d y = v F w S F y F w S F v
79 35 34 76 78 1 brab w R v F w S F v
80 79 a1i F : A 1-1 B w A v A w R v F w S F v
81 f1fveq F : A 1-1 B w A v A F w = F v w = v
82 81 bicomd F : A 1-1 B w A v A w = v F w = F v
83 40 a1i F : A 1-1 B w A v A v R w F v S F w
84 80 82 83 3orbi123d F : A 1-1 B w A v A w R v w = v v R w F w S F v F w = F v F v S F w
85 84 2ralbidva F : A 1-1 B w A v A w R v w = v v R w w A v A F w S F v F w = F v F v S F w
86 breq1 F w = u F w S F v u S F v
87 eqeq1 F w = u F w = F v u = F v
88 breq2 F w = u F v S F w F v S u
89 86 87 88 3orbi123d F w = u F w S F v F w = F v F v S F w u S F v u = F v F v S u
90 89 ralbidv F w = u v A F w S F v F w = F v F v S F w v A u S F v u = F v F v S u
91 90 cbvfo F : A onto B w A v A F w S F v F w = F v F v S F w u B v A u S F v u = F v F v S u
92 breq2 F v = f u S F v u S f
93 eqeq2 F v = f u = F v u = f
94 breq1 F v = f F v S u f S u
95 92 93 94 3orbi123d F v = f u S F v u = F v F v S u u S f u = f f S u
96 95 cbvfo F : A onto B v A u S F v u = F v F v S u f B u S f u = f f S u
97 96 ralbidv F : A onto B u B v A u S F v u = F v F v S u u B f B u S f u = f f S u
98 91 97 bitrd F : A onto B w A v A F w S F v F w = F v F v S F w u B f B u S f u = f f S u
99 85 98 sylan9bb F : A 1-1 B F : A onto B w A v A w R v w = v v R w u B f B u S f u = f f S u
100 74 99 sylbi F : A 1-1 onto B w A v A w R v w = v v R w u B f B u S f u = f f S u
101 100 biimprd F : A 1-1 onto B u B f B u S f u = f f S u w A v A w R v w = v v R w
102 73 101 anim12d F : A 1-1 onto B S Fr B u B f B u S f u = f f S u R Fr A w A v A w R v w = v v R w
103 dfwe2 S We B S Fr B u B f B u S f u = f f S u
104 dfwe2 R We A R Fr A w A v A w R v w = v v R w
105 102 103 104 3imtr4g F : A 1-1 onto B S We B R We A