Step | Hyp | Ref
| Expression |
1 | | pm3.24 393 |
. 2
⊢ ¬
(ran 𝐹 ∈ V ∧ ¬
ran 𝐹 ∈
V) |
2 | | df-ne 2970 |
. . . . 5
⊢ (𝐷 ≠ ∅ ↔ ¬ 𝐷 = ∅) |
3 | 2 | ralbii 3162 |
. . . 4
⊢
(∀𝑥 ∈ On
𝐷 ≠ ∅ ↔
∀𝑥 ∈ On ¬
𝐷 =
∅) |
4 | | df-ral 3095 |
. . . 4
⊢
(∀𝑥 ∈ On
𝐷 ≠ ∅ ↔
∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) |
5 | | ralnex 3174 |
. . . 4
⊢
(∀𝑥 ∈ On
¬ 𝐷 = ∅ ↔
¬ ∃𝑥 ∈ On
𝐷 =
∅) |
6 | 3, 4, 5 | 3bitr3i 293 |
. . 3
⊢
(∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) ↔ ¬
∃𝑥 ∈ On 𝐷 = ∅) |
7 | | weso 5346 |
. . . . . . . . 9
⊢ (𝑤 We 𝐴 → 𝑤 Or 𝐴) |
8 | 7 | adantr 474 |
. . . . . . . 8
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → 𝑤 Or 𝐴) |
9 | | vex 3401 |
. . . . . . . 8
⊢ 𝑤 ∈ V |
10 | | soex 7388 |
. . . . . . . 8
⊢ ((𝑤 Or 𝐴 ∧ 𝑤 ∈ V) → 𝐴 ∈ V) |
11 | 8, 9, 10 | sylancl 580 |
. . . . . . 7
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → 𝐴 ∈ V) |
12 | | zorn2lem.3 |
. . . . . . . . . . 11
⊢ 𝐹 = recs((𝑓 ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑤𝑣))) |
13 | 12 | tfr1 7776 |
. . . . . . . . . 10
⊢ 𝐹 Fn On |
14 | | fvelrnb 6503 |
. . . . . . . . . 10
⊢ (𝐹 Fn On → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ On (𝐹‘𝑥) = 𝑦)) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ On (𝐹‘𝑥) = 𝑦) |
16 | | nfv 1957 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑤 We 𝐴 |
17 | | nfa1 2145 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) |
18 | 16, 17 | nfan 1946 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) |
19 | | nfv 1957 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
20 | | zorn2lem.5 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} |
21 | 20 | ssrab3 3909 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐷 ⊆ 𝐴 |
22 | | zorn2lem.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐶 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧} |
23 | 12, 22, 20 | zorn2lem1 9653 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ On ∧ (𝑤 We 𝐴 ∧ 𝐷 ≠ ∅)) → (𝐹‘𝑥) ∈ 𝐷) |
24 | 21, 23 | sseldi 3819 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ (𝑤 We 𝐴 ∧ 𝐷 ≠ ∅)) → (𝐹‘𝑥) ∈ 𝐴) |
25 | | eleq1 2847 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
26 | 24, 25 | syl5ibcom 237 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ (𝑤 We 𝐴 ∧ 𝐷 ≠ ∅)) → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)) |
27 | 26 | exp32 413 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ On → (𝑤 We 𝐴 → (𝐷 ≠ ∅ → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)))) |
28 | 27 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑤 We 𝐴 → (𝑥 ∈ On → (𝐷 ≠ ∅ → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)))) |
29 | 28 | a2d 29 |
. . . . . . . . . . . 12
⊢ (𝑤 We 𝐴 → ((𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)))) |
30 | 29 | spsd 2171 |
. . . . . . . . . . 11
⊢ (𝑤 We 𝐴 → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)))) |
31 | 30 | imp 397 |
. . . . . . . . . 10
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (𝑥 ∈ On → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴))) |
32 | 18, 19, 31 | rexlimd 3208 |
. . . . . . . . 9
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (∃𝑥 ∈ On (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)) |
33 | 15, 32 | syl5bi 234 |
. . . . . . . 8
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐴)) |
34 | 33 | ssrdv 3827 |
. . . . . . 7
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → ran 𝐹 ⊆ 𝐴) |
35 | 11, 34 | ssexd 5042 |
. . . . . 6
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → ran 𝐹 ∈ V) |
36 | 35 | ex 403 |
. . . . 5
⊢ (𝑤 We 𝐴 → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ran 𝐹 ∈ V)) |
37 | 36 | adantl 475 |
. . . 4
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ran 𝐹 ∈ V)) |
38 | 12, 22, 20 | zorn2lem3 9655 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Po 𝐴 ∧ (𝑥 ∈ On ∧ (𝑤 We 𝐴 ∧ 𝐷 ≠ ∅))) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
39 | 38 | exp45 431 |
. . . . . . . . . . . . 13
⊢ (𝑅 Po 𝐴 → (𝑥 ∈ On → (𝑤 We 𝐴 → (𝐷 ≠ ∅ → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))))) |
40 | 39 | com23 86 |
. . . . . . . . . . . 12
⊢ (𝑅 Po 𝐴 → (𝑤 We 𝐴 → (𝑥 ∈ On → (𝐷 ≠ ∅ → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))))) |
41 | 40 | imp 397 |
. . . . . . . . . . 11
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (𝑥 ∈ On → (𝐷 ≠ ∅ → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) |
42 | 41 | a2d 29 |
. . . . . . . . . 10
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) |
43 | 42 | imp4a 415 |
. . . . . . . . 9
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
44 | 43 | alrimdv 1972 |
. . . . . . . 8
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
45 | 44 | alimdv 1959 |
. . . . . . 7
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑥∀𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
46 | | r2al 3121 |
. . . . . . 7
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
47 | 45, 46 | syl6ibr 244 |
. . . . . 6
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑥 ∈ On ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
48 | | ssid 3842 |
. . . . . . . 8
⊢ On
⊆ On |
49 | 13 | tz7.48lem 7819 |
. . . . . . . 8
⊢ ((On
⊆ On ∧ ∀𝑥
∈ On ∀𝑦 ∈
𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ On)) |
50 | 48, 49 | mpan 680 |
. . . . . . 7
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → Fun ◡(𝐹 ↾ On)) |
51 | | fnrel 6234 |
. . . . . . . . . . 11
⊢ (𝐹 Fn On → Rel 𝐹) |
52 | 13, 51 | ax-mp 5 |
. . . . . . . . . 10
⊢ Rel 𝐹 |
53 | | fndm 6235 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn On → dom 𝐹 = On) |
54 | 13, 53 | ax-mp 5 |
. . . . . . . . . . 11
⊢ dom 𝐹 = On |
55 | 54 | eqimssi 3878 |
. . . . . . . . . 10
⊢ dom 𝐹 ⊆ On |
56 | | relssres 5687 |
. . . . . . . . . 10
⊢ ((Rel
𝐹 ∧ dom 𝐹 ⊆ On) → (𝐹 ↾ On) = 𝐹) |
57 | 52, 55, 56 | mp2an 682 |
. . . . . . . . 9
⊢ (𝐹 ↾ On) = 𝐹 |
58 | 57 | cnveqi 5542 |
. . . . . . . 8
⊢ ◡(𝐹 ↾ On) = ◡𝐹 |
59 | 58 | funeqi 6156 |
. . . . . . 7
⊢ (Fun
◡(𝐹 ↾ On) ↔ Fun ◡𝐹) |
60 | 50, 59 | sylib 210 |
. . . . . 6
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → Fun ◡𝐹) |
61 | 47, 60 | syl6 35 |
. . . . 5
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → Fun ◡𝐹)) |
62 | | onprc 7262 |
. . . . . 6
⊢ ¬ On
∈ V |
63 | | funrnex 7412 |
. . . . . . . 8
⊢ (dom
◡𝐹 ∈ V → (Fun ◡𝐹 → ran ◡𝐹 ∈ V)) |
64 | 63 | com12 32 |
. . . . . . 7
⊢ (Fun
◡𝐹 → (dom ◡𝐹 ∈ V → ran ◡𝐹 ∈ V)) |
65 | | df-rn 5366 |
. . . . . . . 8
⊢ ran 𝐹 = dom ◡𝐹 |
66 | 65 | eleq1i 2850 |
. . . . . . 7
⊢ (ran
𝐹 ∈ V ↔ dom ◡𝐹 ∈ V) |
67 | | dfdm4 5561 |
. . . . . . . . 9
⊢ dom 𝐹 = ran ◡𝐹 |
68 | 54, 67 | eqtr3i 2804 |
. . . . . . . 8
⊢ On = ran
◡𝐹 |
69 | 68 | eleq1i 2850 |
. . . . . . 7
⊢ (On
∈ V ↔ ran ◡𝐹 ∈ V) |
70 | 64, 66, 69 | 3imtr4g 288 |
. . . . . 6
⊢ (Fun
◡𝐹 → (ran 𝐹 ∈ V → On ∈
V)) |
71 | 62, 70 | mtoi 191 |
. . . . 5
⊢ (Fun
◡𝐹 → ¬ ran 𝐹 ∈ V) |
72 | 61, 71 | syl6 35 |
. . . 4
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ¬ ran 𝐹 ∈ V)) |
73 | 37, 72 | jcad 508 |
. . 3
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V))) |
74 | 6, 73 | syl5bir 235 |
. 2
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (¬ ∃𝑥 ∈ On 𝐷 = ∅ → (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V))) |
75 | 1, 74 | mt3i 144 |
1
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ∃𝑥 ∈ On 𝐷 = ∅) |