Metamath Proof Explorer

Theorem zorn2g

Description: Zorn's Lemma of Monk1 p. 117. This version of zorn2 avoids the Axiom of Choice by assuming that A is well-orderable. (Contributed by NM, 6-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion zorn2g 
|- ( ( A e. dom card /\ R Po A /\ A. w ( ( w C_ A /\ R Or w ) -> E. x e. A A. z e. w ( z R x \/ z = x ) ) ) -> E. x e. A A. y e. A -. x R y )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( g = k -> ( g q n <-> k q n ) )
2 1 notbid 
 |-  ( g = k -> ( -. g q n <-> -. k q n ) )
3 2 cbvralvw 
 |-  ( A. g e. { v e. A | A. q e. ran h q R v } -. g q n <-> A. k e. { v e. A | A. q e. ran h q R v } -. k q n )
4 breq2 
 |-  ( n = m -> ( k q n <-> k q m ) )
5 4 notbid 
 |-  ( n = m -> ( -. k q n <-> -. k q m ) )
6 5 ralbidv 
 |-  ( n = m -> ( A. k e. { v e. A | A. q e. ran h q R v } -. k q n <-> A. k e. { v e. A | A. q e. ran h q R v } -. k q m ) )
7 3 6 syl5bb 
 |-  ( n = m -> ( A. g e. { v e. A | A. q e. ran h q R v } -. g q n <-> A. k e. { v e. A | A. q e. ran h q R v } -. k q m ) )
8 7 cbvriotavw 
 |-  ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) = ( iota_ m e. { v e. A | A. q e. ran h q R v } A. k e. { v e. A | A. q e. ran h q R v } -. k q m )
9 rneq 
 |-  ( h = d -> ran h = ran d )
10 9 raleqdv 
 |-  ( h = d -> ( A. q e. ran h q R v <-> A. q e. ran d q R v ) )
11 10 rabbidv 
 |-  ( h = d -> { v e. A | A. q e. ran h q R v } = { v e. A | A. q e. ran d q R v } )
12 11 raleqdv 
 |-  ( h = d -> ( A. k e. { v e. A | A. q e. ran h q R v } -. k q m <-> A. k e. { v e. A | A. q e. ran d q R v } -. k q m ) )
13 11 12 riotaeqbidv 
 |-  ( h = d -> ( iota_ m e. { v e. A | A. q e. ran h q R v } A. k e. { v e. A | A. q e. ran h q R v } -. k q m ) = ( iota_ m e. { v e. A | A. q e. ran d q R v } A. k e. { v e. A | A. q e. ran d q R v } -. k q m ) )
14 8 13 eqtrid 
 |-  ( h = d -> ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) = ( iota_ m e. { v e. A | A. q e. ran d q R v } A. k e. { v e. A | A. q e. ran d q R v } -. k q m ) )
15 14 cbvmptv 
 |-  ( h e. _V |-> ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) ) = ( d e. _V |-> ( iota_ m e. { v e. A | A. q e. ran d q R v } A. k e. { v e. A | A. q e. ran d q R v } -. k q m ) )
16 recseq 
 |-  ( ( h e. _V |-> ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) ) = ( d e. _V |-> ( iota_ m e. { v e. A | A. q e. ran d q R v } A. k e. { v e. A | A. q e. ran d q R v } -. k q m ) ) -> recs ( ( h e. _V |-> ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) ) ) = recs ( ( d e. _V |-> ( iota_ m e. { v e. A | A. q e. ran d q R v } A. k e. { v e. A | A. q e. ran d q R v } -. k q m ) ) ) )
17 15 16 ax-mp 
 |-  recs ( ( h e. _V |-> ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) ) ) = recs ( ( d e. _V |-> ( iota_ m e. { v e. A | A. q e. ran d q R v } A. k e. { v e. A | A. q e. ran d q R v } -. k q m ) ) )
18 breq1 
 |-  ( q = s -> ( q R v <-> s R v ) )
19 18 cbvralvw 
 |-  ( A. q e. ran d q R v <-> A. s e. ran d s R v )
20 breq2 
 |-  ( v = r -> ( s R v <-> s R r ) )
21 20 ralbidv 
 |-  ( v = r -> ( A. s e. ran d s R v <-> A. s e. ran d s R r ) )
22 19 21 syl5bb 
 |-  ( v = r -> ( A. q e. ran d q R v <-> A. s e. ran d s R r ) )
23 22 cbvrabv 
 |-  { v e. A | A. q e. ran d q R v } = { r e. A | A. s e. ran d s R r }
24 eqid 
 |-  { r e. A | A. s e. ( recs ( ( h e. _V |-> ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) ) ) " u ) s R r } = { r e. A | A. s e. ( recs ( ( h e. _V |-> ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) ) ) " u ) s R r }
25 eqid 
 |-  { r e. A | A. s e. ( recs ( ( h e. _V |-> ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) ) ) " t ) s R r } = { r e. A | A. s e. ( recs ( ( h e. _V |-> ( iota_ n e. { v e. A | A. q e. ran h q R v } A. g e. { v e. A | A. q e. ran h q R v } -. g q n ) ) ) " t ) s R r }
26 17 23 24 25 zorn2lem7 
 |-  ( ( A e. dom card /\ R Po A /\ A. w ( ( w C_ A /\ R Or w ) -> E. x e. A A. z e. w ( z R x \/ z = x ) ) ) -> E. x e. A A. y e. A -. x R y )