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