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

Metamath Proof Explorer

Theorem zorn2lem5

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

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

Proof

Step Hyp Ref Expression
1 zorn2lem.3 ⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2 zorn2lem.4 ⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3 zorn2lem.5 ⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
4 zorn2lem.7 ⊢ 𝐻 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑦 ) 𝑔 𝑅 𝑧 }
5 1 tfr1 ⊢ 𝐹 Fn On
6 fnfun ⊢ ( 𝐹 Fn On → Fun 𝐹 )
7 5 6 ax-mp ⊢ Fun 𝐹
8 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑠 ∈ ( 𝐹 “ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑠 )
9 7 8 mpan ⊢ ( 𝑠 ∈ ( 𝐹 “ 𝑥 ) → ∃ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑠 )
10 nfv ⊢ Ⅎ 𝑦 ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On )
11 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅
12 10 11 nfan ⊢ Ⅎ 𝑦 ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ )
13 nfv ⊢ Ⅎ 𝑦 𝑠 ∈ 𝐴
14 df-ral ⊢ ( ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝐻 ≠ ∅ ) )
15 onelon ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
16 4 ssrab3 ⊢ 𝐻 ⊆ 𝐴
17 1 2 4 zorn2lem1 ⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐻 )
18 16 17 sselid ⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
19 eleq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 ↔ 𝑠 ∈ 𝐴 ) )
20 18 19 imbitrid ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → ( ( 𝑦 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → 𝑠 ∈ 𝐴 ) )
21 15 20 sylani ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → 𝑠 ∈ 𝐴 ) )
22 21 com12 ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 We 𝐴 ∧ 𝐻 ≠ ∅ ) ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) )
23 22 exp43 ⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( 𝑤 We 𝐴 → ( 𝐻 ≠ ∅ → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) ) )
24 23 com3r ⊢ ( 𝑤 We 𝐴 → ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( 𝐻 ≠ ∅ → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) ) )
25 24 imp ⊢ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( 𝑦 ∈ 𝑥 → ( 𝐻 ≠ ∅ → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) )
26 25 a2d ⊢ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( ( 𝑦 ∈ 𝑥 → 𝐻 ≠ ∅ ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) )
27 26 spsd ⊢ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝐻 ≠ ∅ ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) )
28 14 27 biimtrid ⊢ ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) ) )
29 28 imp ⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( 𝑦 ∈ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) ) )
30 12 13 29 rexlimd ⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( ∃ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑠 → 𝑠 ∈ 𝐴 ) )
31 9 30 syl5 ⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( 𝑠 ∈ ( 𝐹 “ 𝑥 ) → 𝑠 ∈ 𝐴 ) )
32 31 ssrdv ⊢ ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → ( 𝐹 “ 𝑥 ) ⊆ 𝐴 )