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

Metamath Proof Explorer

Theorem zorn2lem4

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 zorn2lem4 ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ∃ 𝑥 ∈ On 𝐷 = ∅ )

Proof

Step Hyp Ref Expression
1 zorn2lem.3 ⊢ 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2 zorn2lem.4 ⊢ 𝐶 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3 zorn2lem.5 ⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹 “ 𝑥 ) 𝑔 𝑅 𝑧 }
4 pm3.24 ⊢ ¬ ( ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V )
5 df-ne ⊢ ( 𝐷 ≠ ∅ ↔ ¬ 𝐷 = ∅ )
6 5 ralbii ⊢ ( ∀ 𝑥 ∈ On 𝐷 ≠ ∅ ↔ ∀ 𝑥 ∈ On ¬ 𝐷 = ∅ )
7 df-ral ⊢ ( ∀ 𝑥 ∈ On 𝐷 ≠ ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) )
8 ralnex ⊢ ( ∀ 𝑥 ∈ On ¬ 𝐷 = ∅ ↔ ¬ ∃ 𝑥 ∈ On 𝐷 = ∅ )
9 6 7 8 3bitr3i ⊢ ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ↔ ¬ ∃ 𝑥 ∈ On 𝐷 = ∅ )
10 weso ⊢ ( 𝑤 We 𝐴 → 𝑤 Or 𝐴 )
11 10 adantr ⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → 𝑤 Or 𝐴 )
12 vex ⊢ 𝑤 ∈ V
13 soex ⊢ ( ( 𝑤 Or 𝐴 ∧ 𝑤 ∈ V ) → 𝐴 ∈ V )
14 11 12 13 sylancl ⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → 𝐴 ∈ V )
15 1 tfr1 ⊢ 𝐹 Fn On
16 fvelrnb ⊢ ( 𝐹 Fn On → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
17 15 16 ax-mp ⊢ ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) = 𝑦 )
18 nfv ⊢ Ⅎ 𝑥 𝑤 We 𝐴
19 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ )
20 18 19 nfan ⊢ Ⅎ 𝑥 ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) )
21 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
22 3 ssrab3 ⊢ 𝐷 ⊆ 𝐴
23 1 2 3 zorn2lem1 ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
24 22 23 sselid ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 )
25 eleq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
26 24 25 syl5ibcom ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) )
27 26 exp32 ⊢ ( 𝑥 ∈ On → ( 𝑤 We 𝐴 → ( 𝐷 ≠ ∅ → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
28 27 com12 ⊢ ( 𝑤 We 𝐴 → ( 𝑥 ∈ On → ( 𝐷 ≠ ∅ → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
29 28 a2d ⊢ ( 𝑤 We 𝐴 → ( ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( 𝑥 ∈ On → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
30 29 spsd ⊢ ( 𝑤 We 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( 𝑥 ∈ On → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
31 30 imp ⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ( 𝑥 ∈ On → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) ) )
32 20 21 31 rexlimd ⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ( ∃ 𝑥 ∈ On ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝐴 ) )
33 17 32 biimtrid ⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐴 ) )
34 33 ssrdv ⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ran 𝐹 ⊆ 𝐴 )
35 14 34 ssexd ⊢ ( ( 𝑤 We 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) ) → ran 𝐹 ∈ V )
36 35 ex ⊢ ( 𝑤 We 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ran 𝐹 ∈ V ) )
37 36 adantl ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ran 𝐹 ∈ V ) )
38 1 2 3 zorn2lem3 ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑥 ∈ On ∧ ( 𝑤 We 𝐴 ∧ 𝐷 ≠ ∅ ) ) ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
39 38 exp45 ⊢ ( 𝑅 Po 𝐴 → ( 𝑥 ∈ On → ( 𝑤 We 𝐴 → ( 𝐷 ≠ ∅ → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
40 39 com23 ⊢ ( 𝑅 Po 𝐴 → ( 𝑤 We 𝐴 → ( 𝑥 ∈ On → ( 𝐷 ≠ ∅ → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
41 40 imp ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( 𝑥 ∈ On → ( 𝐷 ≠ ∅ → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) )
42 41 a2d ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) )
43 42 imp4a ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
44 43 alrimdv ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ∀ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
45 44 alimdv ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
46 r2al ⊢ ( ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
47 45 46 imbitrrdi ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
48 ssid ⊢ On ⊆ On
49 15 tz7.48lem ⊢ ( ( On ⊆ On ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ On ) )
50 48 49 mpan ⊢ ( ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → Fun ◡ ( 𝐹 ↾ On ) )
51 fnrel ⊢ ( 𝐹 Fn On → Rel 𝐹 )
52 15 51 ax-mp ⊢ Rel 𝐹
53 15 fndmi ⊢ dom 𝐹 = On
54 53 eqimssi ⊢ dom 𝐹 ⊆ On
55 relssres ⊢ ( ( Rel 𝐹 ∧ dom 𝐹 ⊆ On ) → ( 𝐹 ↾ On ) = 𝐹 )
56 52 54 55 mp2an ⊢ ( 𝐹 ↾ On ) = 𝐹
57 56 cnveqi ⊢ ◡ ( 𝐹 ↾ On ) = ◡ 𝐹
58 57 funeqi ⊢ ( Fun ◡ ( 𝐹 ↾ On ) ↔ Fun ◡ 𝐹 )
59 50 58 sylib ⊢ ( ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → Fun ◡ 𝐹 )
60 47 59 syl6 ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → Fun ◡ 𝐹 ) )
61 onprc ⊢ ¬ On ∈ V
62 funrnex ⊢ ( dom ◡ 𝐹 ∈ V → ( Fun ◡ 𝐹 → ran ◡ 𝐹 ∈ V ) )
63 62 com12 ⊢ ( Fun ◡ 𝐹 → ( dom ◡ 𝐹 ∈ V → ran ◡ 𝐹 ∈ V ) )
64 df-rn ⊢ ran 𝐹 = dom ◡ 𝐹
65 64 eleq1i ⊢ ( ran 𝐹 ∈ V ↔ dom ◡ 𝐹 ∈ V )
66 dfdm4 ⊢ dom 𝐹 = ran ◡ 𝐹
67 53 66 eqtr3i ⊢ On = ran ◡ 𝐹
68 67 eleq1i ⊢ ( On ∈ V ↔ ran ◡ 𝐹 ∈ V )
69 63 65 68 3imtr4g ⊢ ( Fun ◡ 𝐹 → ( ran 𝐹 ∈ V → On ∈ V ) )
70 61 69 mtoi ⊢ ( Fun ◡ 𝐹 → ¬ ran 𝐹 ∈ V )
71 60 70 syl6 ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ¬ ran 𝐹 ∈ V ) )
72 37 71 jcad ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ∀ 𝑥 ( 𝑥 ∈ On → 𝐷 ≠ ∅ ) → ( ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V ) ) )
73 9 72 biimtrrid ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ( ¬ ∃ 𝑥 ∈ On 𝐷 = ∅ → ( ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V ) ) )
74 4 73 mt3i ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑤 We 𝐴 ) → ∃ 𝑥 ∈ On 𝐷 = ∅ )