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

Metamath Proof Explorer

Theorem zorn2lem2

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 zorn2lem2 ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 zorn2lem.3 ⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2 zorn2lem.4 ⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3 zorn2lem.5 ⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
4 1 2 3 zorn2lem1 ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
5 breq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( 𝑔 𝑅 𝑧 ↔ 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
6 5 ralbidv ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 ↔ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
7 6 3 elrab2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ∧ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
8 7 simprbi ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 → ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) )
9 4 8 syl ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) )
10 1 tfr1 ⊢ 𝐹 Fn On
11 onss ⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
12 fnfvima ⊢ ( ( 𝐹 Fn On ∧ 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) )
13 12 3expia ⊢ ( ( 𝐹 Fn On ∧ 𝑥 ⊆ On ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) ) )
14 10 11 13 sylancr ⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) ) )
15 14 adantr ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) ) )
16 breq1 ⊢ ( 𝑔 = ( 𝐹 ‘ 𝑦 ) → ( 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
17 16 rspccv ⊢ ( ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )
18 9 15 17 sylsyld ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑥 ) ) )