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∈dom⁡card∧RPoA∧∀ww⊆A∧ROrw→∃x∈A∀z∈wzRx∨z=x→∃x∈A∀y∈A¬xRy

Proof

Step Hyp Ref Expression
1 breq1 ⊢g=k→gqn↔kqn
2 1 notbid ⊢g=k→¬gqn↔¬kqn
3 2 cbvralvw ⊢∀g∈v∈A|∀q∈ran⁡hqRv¬gqn↔∀k∈v∈A|∀q∈ran⁡hqRv¬kqn
4 breq2 ⊢n=m→kqn↔kqm
5 4 notbid ⊢n=m→¬kqn↔¬kqm
6 5 ralbidv ⊢n=m→∀k∈v∈A|∀q∈ran⁡hqRv¬kqn↔∀k∈v∈A|∀q∈ran⁡hqRv¬kqm
7 3 6 bitrid ⊢n=m→∀g∈v∈A|∀q∈ran⁡hqRv¬gqn↔∀k∈v∈A|∀q∈ran⁡hqRv¬kqm
8 7 cbvriotavw ⊢ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqn=ιm∈v∈A|∀q∈ran⁡hqRv|∀k∈v∈A|∀q∈ran⁡hqRv¬kqm
9 rneq ⊢h=d→ran⁡h=ran⁡d
10 9 raleqdv ⊢h=d→∀q∈ran⁡hqRv↔∀q∈ran⁡dqRv
11 10 rabbidv ⊢h=d→v∈A|∀q∈ran⁡hqRv=v∈A|∀q∈ran⁡dqRv
12 11 raleqdv ⊢h=d→∀k∈v∈A|∀q∈ran⁡hqRv¬kqm↔∀k∈v∈A|∀q∈ran⁡dqRv¬kqm
13 11 12 riotaeqbidv ⊢h=d→ιm∈v∈A|∀q∈ran⁡hqRv|∀k∈v∈A|∀q∈ran⁡hqRv¬kqm=ιm∈v∈A|∀q∈ran⁡dqRv|∀k∈v∈A|∀q∈ran⁡dqRv¬kqm
14 8 13 eqtrid ⊢h=d→ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqn=ιm∈v∈A|∀q∈ran⁡dqRv|∀k∈v∈A|∀q∈ran⁡dqRv¬kqm
15 14 cbvmptv ⊢h∈V⟼ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqn=d∈V⟼ιm∈v∈A|∀q∈ran⁡dqRv|∀k∈v∈A|∀q∈ran⁡dqRv¬kqm
16 recseq ⊢h∈V⟼ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqn=d∈V⟼ιm∈v∈A|∀q∈ran⁡dqRv|∀k∈v∈A|∀q∈ran⁡dqRv¬kqm→recs⁡h∈V⟼ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqn=recs⁡d∈V⟼ιm∈v∈A|∀q∈ran⁡dqRv|∀k∈v∈A|∀q∈ran⁡dqRv¬kqm
17 15 16 ax-mp ⊢recs⁡h∈V⟼ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqn=recs⁡d∈V⟼ιm∈v∈A|∀q∈ran⁡dqRv|∀k∈v∈A|∀q∈ran⁡dqRv¬kqm
18 breq1 ⊢q=s→qRv↔sRv
19 18 cbvralvw ⊢∀q∈ran⁡dqRv↔∀s∈ran⁡dsRv
20 breq2 ⊢v=r→sRv↔sRr
21 20 ralbidv ⊢v=r→∀s∈ran⁡dsRv↔∀s∈ran⁡dsRr
22 19 21 bitrid ⊢v=r→∀q∈ran⁡dqRv↔∀s∈ran⁡dsRr
23 22 cbvrabv ⊢v∈A|∀q∈ran⁡dqRv=r∈A|∀s∈ran⁡dsRr
24 eqid ⊢r∈A|∀s∈recs⁡h∈V⟼ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqnusRr=r∈A|∀s∈recs⁡h∈V⟼ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqnusRr
25 eqid ⊢r∈A|∀s∈recs⁡h∈V⟼ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqntsRr=r∈A|∀s∈recs⁡h∈V⟼ιn∈v∈A|∀q∈ran⁡hqRv|∀g∈v∈A|∀q∈ran⁡hqRv¬gqntsRr
26 17 23 24 25 zorn2lem7 ⊢A∈dom⁡card∧RPoA∧∀ww⊆A∧ROrw→∃x∈A∀z∈wzRx∨z=x→∃x∈A∀y∈A¬xRy