Theorem zorn2lem3

Description: Lemma for zorn2 . (Contributed by NM, 3-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

	Ref	Expression
Hypotheses	zorn2lem.3	⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
	zorn2lem.4	⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
	zorn2lem.5	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
Assertion	zorn2lem3	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zorn2lem.3	⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2		zorn2lem.4	⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3		zorn2lem.5	⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
4	1 2 3	zorn2lem2	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
5	4	adantl	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
6	3	ssrab3	⊢ 𝐷 ⊆ 𝐴
7	1 2 3	zorn2lem1	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
8	6 7	sselid	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 )
9		breq1	⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
10	9	biimprcd	⊢ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
11		poirr	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) → ¬ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑥 ) )
12	10 11	nsyli	⊢ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) → ( ( 𝑅 Po 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
13	12	com12	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
14	8 13	sylan2	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
15	5 14	syld	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )