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	syl5eq	⊢ ( ℎ = 𝑑 → ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ 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 𝑤 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝑤 ( 𝑧 𝑅 𝑥 ∨ 𝑧 = 𝑥 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 )