Metamath Proof Explorer


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 𝐴𝐷 ≠ ∅ ) ) ) → ( 𝑦𝑥 → ¬ ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ) )