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 ( ( 𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀ 𝑤 ( ( 𝑤𝐴𝑅 Or 𝑤 ) → ∃ 𝑥𝐴𝑧𝑤 ( 𝑧 𝑅 𝑥𝑧 = 𝑥 ) ) ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 )

Proof

Step Hyp Ref Expression
1 breq1 ( 𝑔 = 𝑘 → ( 𝑔 𝑞 𝑛𝑘 𝑞 𝑛 ) )
2 1 notbid ( 𝑔 = 𝑘 → ( ¬ 𝑔 𝑞 𝑛 ↔ ¬ 𝑘 𝑞 𝑛 ) )
3 2 cbvralvw ( ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ↔ ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑛 )
4 breq2 ( 𝑛 = 𝑚 → ( 𝑘 𝑞 𝑛𝑘 𝑞 𝑚 ) )
5 4 notbid ( 𝑛 = 𝑚 → ( ¬ 𝑘 𝑞 𝑛 ↔ ¬ 𝑘 𝑞 𝑚 ) )
6 5 ralbidv ( 𝑛 = 𝑚 → ( ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑛 ↔ ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) )
7 3 6 syl5bb ( 𝑛 = 𝑚 → ( ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ↔ ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) )
8 7 cbvriotavw ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) = ( 𝑚 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 )
9 rneq ( = 𝑑 → ran = ran 𝑑 )
10 9 raleqdv ( = 𝑑 → ( ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 ↔ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 ) )
11 10 rabbidv ( = 𝑑 → { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } = { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } )
12 11 raleqdv ( = 𝑑 → ( ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ↔ ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) )
13 11 12 riotaeqbidv ( = 𝑑 → ( 𝑚 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) = ( 𝑚 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) )
14 8 13 eqtrid ( = 𝑑 → ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) = ( 𝑚 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) )
15 14 cbvmptv ( ∈ V ↦ ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) = ( 𝑑 ∈ V ↦ ( 𝑚 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) )
16 recseq ( ( ∈ V ↦ ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) = ( 𝑑 ∈ V ↦ ( 𝑚 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) → recs ( ( ∈ V ↦ ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) = recs ( ( 𝑑 ∈ V ↦ ( 𝑚 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) ) )
17 15 16 ax-mp recs ( ( ∈ V ↦ ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) = recs ( ( 𝑑 ∈ V ↦ ( 𝑚 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) )
18 breq1 ( 𝑞 = 𝑠 → ( 𝑞 𝑅 𝑣𝑠 𝑅 𝑣 ) )
19 18 cbvralvw ( ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 ↔ ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑣 )
20 breq2 ( 𝑣 = 𝑟 → ( 𝑠 𝑅 𝑣𝑠 𝑅 𝑟 ) )
21 20 ralbidv ( 𝑣 = 𝑟 → ( ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑣 ↔ ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑟 ) )
22 19 21 syl5bb ( 𝑣 = 𝑟 → ( ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 ↔ ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑟 ) )
23 22 cbvrabv { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } = { 𝑟𝐴 ∣ ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑟 }
24 eqid { 𝑟𝐴 ∣ ∀ 𝑠 ∈ ( recs ( ( ∈ V ↦ ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) “ 𝑢 ) 𝑠 𝑅 𝑟 } = { 𝑟𝐴 ∣ ∀ 𝑠 ∈ ( recs ( ( ∈ V ↦ ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) “ 𝑢 ) 𝑠 𝑅 𝑟 }
25 eqid { 𝑟𝐴 ∣ ∀ 𝑠 ∈ ( recs ( ( ∈ V ↦ ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) “ 𝑡 ) 𝑠 𝑅 𝑟 } = { 𝑟𝐴 ∣ ∀ 𝑠 ∈ ( recs ( ( ∈ V ↦ ( 𝑛 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣𝐴 ∣ ∀ 𝑞 ∈ ran 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) “ 𝑡 ) 𝑠 𝑅 𝑟 }
26 17 23 24 25 zorn2lem7 ( ( 𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀ 𝑤 ( ( 𝑤𝐴𝑅 Or 𝑤 ) → ∃ 𝑥𝐴𝑧𝑤 ( 𝑧 𝑅 𝑥𝑧 = 𝑥 ) ) ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 )