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 ∧ R Po A ∧ ∀ w w ⊆ A ∧ R Or w → ∃ x ∈ A ∀ z ∈ w z R x ∨ z = x → ∃ x ∈ A ∀ y ∈ 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 ⊢ ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n ↔ ∀ k ∈ v ∈ A | ∀ q ∈ 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 → ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ k q n ↔ ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ k q m
7 3 6 syl5bb ⊢ n = m → ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n ↔ ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ k q m
8 7 cbvriotavw ⊢ ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n = ι m ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ k q m
9 rneq ⊢ h = d → ran ⁡ h = ran ⁡ d
10 9 raleqdv ⊢ h = d → ∀ q ∈ ran ⁡ h q R v ↔ ∀ q ∈ ran ⁡ d q R v
11 10 rabbidv ⊢ h = d → v ∈ A | ∀ q ∈ ran ⁡ h q R v = v ∈ A | ∀ q ∈ ran ⁡ d q R v
12 11 raleqdv ⊢ h = d → ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ k q m ↔ ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v ¬ k q m
13 11 12 riotaeqbidv ⊢ h = d → ι m ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ k q m = ι m ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v | ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v ¬ k q m
14 8 13 syl5eq ⊢ h = d → ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n = ι m ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v | ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v ¬ k q m
15 14 cbvmptv ⊢ h ∈ V ⟼ ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n = d ∈ V ⟼ ι m ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v | ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v ¬ k q m
16 recseq ⊢ h ∈ V ⟼ ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n = d ∈ V ⟼ ι m ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v | ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v ¬ k q m → recs ⁡ h ∈ V ⟼ ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n = recs ⁡ d ∈ V ⟼ ι m ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v | ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v ¬ k q m
17 15 16 ax-mp ⊢ recs ⁡ h ∈ V ⟼ ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n = recs ⁡ d ∈ V ⟼ ι m ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v | ∀ k ∈ v ∈ A | ∀ q ∈ ran ⁡ d q R v ¬ k q m
18 breq1 ⊢ q = s → q R v ↔ s R v
19 18 cbvralvw ⊢ ∀ q ∈ ran ⁡ d q R v ↔ ∀ s ∈ ran ⁡ d s R v
20 breq2 ⊢ v = r → s R v ↔ s R r
21 20 ralbidv ⊢ v = r → ∀ s ∈ ran ⁡ d s R v ↔ ∀ s ∈ ran ⁡ d s R r
22 19 21 syl5bb ⊢ v = r → ∀ q ∈ ran ⁡ d q R v ↔ ∀ s ∈ ran ⁡ d s R r
23 22 cbvrabv ⊢ v ∈ A | ∀ q ∈ ran ⁡ d q R v = r ∈ A | ∀ s ∈ ran ⁡ d s R r
24 eqid ⊢ r ∈ A | ∀ s ∈ recs ⁡ h ∈ V ⟼ ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n u s R r = r ∈ A | ∀ s ∈ recs ⁡ h ∈ V ⟼ ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n u s R r
25 eqid ⊢ r ∈ A | ∀ s ∈ recs ⁡ h ∈ V ⟼ ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n t s R r = r ∈ A | ∀ s ∈ recs ⁡ h ∈ V ⟼ ι n ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v | ∀ g ∈ v ∈ A | ∀ q ∈ ran ⁡ h q R v ¬ g q n t s R r
26 17 23 24 25 zorn2lem7 ⊢ A ∈ dom ⁡ card ∧ R Po A ∧ ∀ w w ⊆ A ∧ R Or w → ∃ x ∈ A ∀ z ∈ w z R x ∨ z = x → ∃ x ∈ A ∀ y ∈ A ¬ x R y