This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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