| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pm3.24 402 | . 2
⊢  ¬
(ran 𝐹 ∈ V ∧ ¬
ran 𝐹 ∈
V) | 
| 2 |  | df-ne 2941 | . . . . 5
⊢ (𝐷 ≠ ∅ ↔ ¬ 𝐷 = ∅) | 
| 3 | 2 | ralbii 3093 | . . . 4
⊢
(∀𝑥 ∈ On
𝐷 ≠ ∅ ↔
∀𝑥 ∈ On ¬
𝐷 =
∅) | 
| 4 |  | df-ral 3062 | . . . 4
⊢
(∀𝑥 ∈ On
𝐷 ≠ ∅ ↔
∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) | 
| 5 |  | ralnex 3072 | . . . 4
⊢
(∀𝑥 ∈ On
¬ 𝐷 = ∅ ↔
¬ ∃𝑥 ∈ On
𝐷 =
∅) | 
| 6 | 3, 4, 5 | 3bitr3i 301 | . . 3
⊢
(∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) ↔ ¬
∃𝑥 ∈ On 𝐷 = ∅) | 
| 7 |  | weso 5676 | . . . . . . . . 9
⊢ (𝑤 We 𝐴 → 𝑤 Or 𝐴) | 
| 8 | 7 | adantr 480 | . . . . . . . 8
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → 𝑤 Or 𝐴) | 
| 9 |  | vex 3484 | . . . . . . . 8
⊢ 𝑤 ∈ V | 
| 10 |  | soex 7943 | . . . . . . . 8
⊢ ((𝑤 Or 𝐴 ∧ 𝑤 ∈ V) → 𝐴 ∈ V) | 
| 11 | 8, 9, 10 | sylancl 586 | . . . . . . 7
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → 𝐴 ∈ V) | 
| 12 |  | zorn2lem.3 | . . . . . . . . . . 11
⊢ 𝐹 = recs((𝑓 ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑤𝑣))) | 
| 13 | 12 | tfr1 8437 | . . . . . . . . . 10
⊢ 𝐹 Fn On | 
| 14 |  | fvelrnb 6969 | . . . . . . . . . 10
⊢ (𝐹 Fn On → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ On (𝐹‘𝑥) = 𝑦)) | 
| 15 | 13, 14 | ax-mp 5 | . . . . . . . . 9
⊢ (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ On (𝐹‘𝑥) = 𝑦) | 
| 16 |  | nfv 1914 | . . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑤 We 𝐴 | 
| 17 |  | nfa1 2151 | . . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) | 
| 18 | 16, 17 | nfan 1899 | . . . . . . . . . 10
⊢
Ⅎ𝑥(𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) | 
| 19 |  | nfv 1914 | . . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 | 
| 20 |  | zorn2lem.5 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} | 
| 21 | 20 | ssrab3 4082 | . . . . . . . . . . . . . . . . 17
⊢ 𝐷 ⊆ 𝐴 | 
| 22 |  | zorn2lem.4 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐶 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧} | 
| 23 | 12, 22, 20 | zorn2lem1 10536 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ On ∧ (𝑤 We 𝐴 ∧ 𝐷 ≠ ∅)) → (𝐹‘𝑥) ∈ 𝐷) | 
| 24 | 21, 23 | sselid 3981 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ (𝑤 We 𝐴 ∧ 𝐷 ≠ ∅)) → (𝐹‘𝑥) ∈ 𝐴) | 
| 25 |  | eleq1 2829 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | 
| 26 | 24, 25 | syl5ibcom 245 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ (𝑤 We 𝐴 ∧ 𝐷 ≠ ∅)) → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)) | 
| 27 | 26 | exp32 420 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ On → (𝑤 We 𝐴 → (𝐷 ≠ ∅ → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)))) | 
| 28 | 27 | com12 32 | . . . . . . . . . . . . 13
⊢ (𝑤 We 𝐴 → (𝑥 ∈ On → (𝐷 ≠ ∅ → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)))) | 
| 29 | 28 | a2d 29 | . . . . . . . . . . . 12
⊢ (𝑤 We 𝐴 → ((𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)))) | 
| 30 | 29 | spsd 2187 | . . . . . . . . . . 11
⊢ (𝑤 We 𝐴 → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)))) | 
| 31 | 30 | imp 406 | . . . . . . . . . 10
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (𝑥 ∈ On → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴))) | 
| 32 | 18, 19, 31 | rexlimd 3266 | . . . . . . . . 9
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (∃𝑥 ∈ On (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐴)) | 
| 33 | 15, 32 | biimtrid 242 | . . . . . . . 8
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐴)) | 
| 34 | 33 | ssrdv 3989 | . . . . . . 7
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → ran 𝐹 ⊆ 𝐴) | 
| 35 | 11, 34 | ssexd 5324 | . . . . . 6
⊢ ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → ran 𝐹 ∈ V) | 
| 36 | 35 | ex 412 | . . . . 5
⊢ (𝑤 We 𝐴 → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ran 𝐹 ∈ V)) | 
| 37 | 36 | adantl 481 | . . . 4
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ran 𝐹 ∈ V)) | 
| 38 | 12, 22, 20 | zorn2lem3 10538 | . . . . . . . . . . . . . 14
⊢ ((𝑅 Po 𝐴 ∧ (𝑥 ∈ On ∧ (𝑤 We 𝐴 ∧ 𝐷 ≠ ∅))) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) | 
| 39 | 38 | exp45 438 | . . . . . . . . . . . . 13
⊢ (𝑅 Po 𝐴 → (𝑥 ∈ On → (𝑤 We 𝐴 → (𝐷 ≠ ∅ → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))))) | 
| 40 | 39 | com23 86 | . . . . . . . . . . . 12
⊢ (𝑅 Po 𝐴 → (𝑤 We 𝐴 → (𝑥 ∈ On → (𝐷 ≠ ∅ → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))))) | 
| 41 | 40 | imp 406 | . . . . . . . . . . 11
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (𝑥 ∈ On → (𝐷 ≠ ∅ → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) | 
| 42 | 41 | a2d 29 | . . . . . . . . . 10
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) | 
| 43 | 42 | imp4a 422 | . . . . . . . . 9
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) | 
| 44 | 43 | alrimdv 1929 | . . . . . . . 8
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) | 
| 45 | 44 | alimdv 1916 | . . . . . . 7
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑥∀𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) | 
| 46 |  | r2al 3195 | . . . . . . 7
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) | 
| 47 | 45, 46 | imbitrrdi 252 | . . . . . 6
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑥 ∈ On ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) | 
| 48 |  | ssid 4006 | . . . . . . . 8
⊢ On
⊆ On | 
| 49 | 13 | tz7.48lem 8481 | . . . . . . . 8
⊢ ((On
⊆ On ∧ ∀𝑥
∈ On ∀𝑦 ∈
𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ On)) | 
| 50 | 48, 49 | mpan 690 | . . . . . . 7
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → Fun ◡(𝐹 ↾ On)) | 
| 51 |  | fnrel 6670 | . . . . . . . . . . 11
⊢ (𝐹 Fn On → Rel 𝐹) | 
| 52 | 13, 51 | ax-mp 5 | . . . . . . . . . 10
⊢ Rel 𝐹 | 
| 53 | 13 | fndmi 6672 | . . . . . . . . . . 11
⊢ dom 𝐹 = On | 
| 54 | 53 | eqimssi 4044 | . . . . . . . . . 10
⊢ dom 𝐹 ⊆ On | 
| 55 |  | relssres 6040 | . . . . . . . . . 10
⊢ ((Rel
𝐹 ∧ dom 𝐹 ⊆ On) → (𝐹 ↾ On) = 𝐹) | 
| 56 | 52, 54, 55 | mp2an 692 | . . . . . . . . 9
⊢ (𝐹 ↾ On) = 𝐹 | 
| 57 | 56 | cnveqi 5885 | . . . . . . . 8
⊢ ◡(𝐹 ↾ On) = ◡𝐹 | 
| 58 | 57 | funeqi 6587 | . . . . . . 7
⊢ (Fun
◡(𝐹 ↾ On) ↔ Fun ◡𝐹) | 
| 59 | 50, 58 | sylib 218 | . . . . . 6
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → Fun ◡𝐹) | 
| 60 | 47, 59 | syl6 35 | . . . . 5
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → Fun ◡𝐹)) | 
| 61 |  | onprc 7798 | . . . . . 6
⊢  ¬ On
∈ V | 
| 62 |  | funrnex 7978 | . . . . . . . 8
⊢ (dom
◡𝐹 ∈ V → (Fun ◡𝐹 → ran ◡𝐹 ∈ V)) | 
| 63 | 62 | com12 32 | . . . . . . 7
⊢ (Fun
◡𝐹 → (dom ◡𝐹 ∈ V → ran ◡𝐹 ∈ V)) | 
| 64 |  | df-rn 5696 | . . . . . . . 8
⊢ ran 𝐹 = dom ◡𝐹 | 
| 65 | 64 | eleq1i 2832 | . . . . . . 7
⊢ (ran
𝐹 ∈ V ↔ dom ◡𝐹 ∈ V) | 
| 66 |  | dfdm4 5906 | . . . . . . . . 9
⊢ dom 𝐹 = ran ◡𝐹 | 
| 67 | 53, 66 | eqtr3i 2767 | . . . . . . . 8
⊢ On = ran
◡𝐹 | 
| 68 | 67 | eleq1i 2832 | . . . . . . 7
⊢ (On
∈ V ↔ ran ◡𝐹 ∈ V) | 
| 69 | 63, 65, 68 | 3imtr4g 296 | . . . . . 6
⊢ (Fun
◡𝐹 → (ran 𝐹 ∈ V → On ∈
V)) | 
| 70 | 61, 69 | mtoi 199 | . . . . 5
⊢ (Fun
◡𝐹 → ¬ ran 𝐹 ∈ V) | 
| 71 | 60, 70 | syl6 35 | . . . 4
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ¬ ran 𝐹 ∈ V)) | 
| 72 | 37, 71 | jcad 512 | . . 3
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V))) | 
| 73 | 6, 72 | biimtrrid 243 | . 2
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (¬ ∃𝑥 ∈ On 𝐷 = ∅ → (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V))) | 
| 74 | 1, 73 | mt3i 149 | 1
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ∃𝑥 ∈ On 𝐷 = ∅) |