Metamath Proof Explorer


Theorem zorn2lem1

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

Proof

Step Hyp Ref Expression
1 zorn2lem.3 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2 zorn2lem.4 𝐶 = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3 zorn2lem.5 𝐷 = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑥 ) 𝑔 𝑅 𝑧 }
4 1 tfr2 ( 𝑥 ∈ On → ( 𝐹𝑥 ) = ( ( 𝑓 ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) ) ‘ ( 𝐹𝑥 ) ) )
5 4 adantr ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → ( 𝐹𝑥 ) = ( ( 𝑓 ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) ) ‘ ( 𝐹𝑥 ) ) )
6 1 tfr1 𝐹 Fn On
7 fnfun ( 𝐹 Fn On → Fun 𝐹 )
8 6 7 ax-mp Fun 𝐹
9 vex 𝑥 ∈ V
10 resfunexg ( ( Fun 𝐹𝑥 ∈ V ) → ( 𝐹𝑥 ) ∈ V )
11 8 9 10 mp2an ( 𝐹𝑥 ) ∈ V
12 rneq ( 𝑓 = ( 𝐹𝑥 ) → ran 𝑓 = ran ( 𝐹𝑥 ) )
13 df-ima ( 𝐹𝑥 ) = ran ( 𝐹𝑥 )
14 12 13 eqtr4di ( 𝑓 = ( 𝐹𝑥 ) → ran 𝑓 = ( 𝐹𝑥 ) )
15 14 eleq2d ( 𝑓 = ( 𝐹𝑥 ) → ( 𝑔 ∈ ran 𝑓𝑔 ∈ ( 𝐹𝑥 ) ) )
16 15 imbi1d ( 𝑓 = ( 𝐹𝑥 ) → ( ( 𝑔 ∈ ran 𝑓𝑔 𝑅 𝑧 ) ↔ ( 𝑔 ∈ ( 𝐹𝑥 ) → 𝑔 𝑅 𝑧 ) ) )
17 16 ralbidv2 ( 𝑓 = ( 𝐹𝑥 ) → ( ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 ↔ ∀ 𝑔 ∈ ( 𝐹𝑥 ) 𝑔 𝑅 𝑧 ) )
18 17 rabbidv ( 𝑓 = ( 𝐹𝑥 ) → { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 } = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑥 ) 𝑔 𝑅 𝑧 } )
19 18 2 3 3eqtr4g ( 𝑓 = ( 𝐹𝑥 ) → 𝐶 = 𝐷 )
20 19 eleq2d ( 𝑓 = ( 𝐹𝑥 ) → ( 𝑢𝐶𝑢𝐷 ) )
21 20 imbi1d ( 𝑓 = ( 𝐹𝑥 ) → ( ( 𝑢𝐶 → ¬ 𝑢 𝑤 𝑣 ) ↔ ( 𝑢𝐷 → ¬ 𝑢 𝑤 𝑣 ) ) )
22 21 ralbidv2 ( 𝑓 = ( 𝐹𝑥 ) → ( ∀ 𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ↔ ∀ 𝑢𝐷 ¬ 𝑢 𝑤 𝑣 ) )
23 19 22 riotaeqbidv ( 𝑓 = ( 𝐹𝑥 ) → ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) = ( 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 ) )
24 eqid ( 𝑓 ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) ) = ( 𝑓 ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) )
25 riotaex ( 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 ) ∈ V
26 23 24 25 fvmpt ( ( 𝐹𝑥 ) ∈ V → ( ( 𝑓 ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) ) ‘ ( 𝐹𝑥 ) ) = ( 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 ) )
27 11 26 ax-mp ( ( 𝑓 ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) ) ‘ ( 𝐹𝑥 ) ) = ( 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 )
28 5 27 eqtrdi ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → ( 𝐹𝑥 ) = ( 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 ) )
29 simprl ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → 𝑤 We 𝐴 )
30 weso ( 𝑤 We 𝐴𝑤 Or 𝐴 )
31 30 ad2antrl ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → 𝑤 Or 𝐴 )
32 vex 𝑤 ∈ V
33 soex ( ( 𝑤 Or 𝐴𝑤 ∈ V ) → 𝐴 ∈ V )
34 31 32 33 sylancl ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → 𝐴 ∈ V )
35 3 34 rabexd ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → 𝐷 ∈ V )
36 3 ssrab3 𝐷𝐴
37 36 a1i ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → 𝐷𝐴 )
38 simprr ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → 𝐷 ≠ ∅ )
39 wereu ( ( 𝑤 We 𝐴 ∧ ( 𝐷 ∈ V ∧ 𝐷𝐴𝐷 ≠ ∅ ) ) → ∃! 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 )
40 29 35 37 38 39 syl13anc ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → ∃! 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 )
41 riotacl ( ∃! 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 → ( 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 ) ∈ 𝐷 )
42 40 41 syl ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → ( 𝑣𝐷𝑢𝐷 ¬ 𝑢 𝑤 𝑣 ) ∈ 𝐷 )
43 28 42 eqeltrd ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴𝐷 ≠ ∅ ) ) → ( 𝐹𝑥 ) ∈ 𝐷 )