| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnfoctb 45058 | . 2
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) →
∃𝑔 𝑔:ℕ–onto→𝐴) | 
| 2 |  | fofn 6821 | . . . . . 6
⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ) | 
| 3 |  | nnex 12273 | . . . . . . 7
⊢ ℕ
∈ V | 
| 4 | 3 | a1i 11 | . . . . . 6
⊢ (𝑔:ℕ–onto→𝐴 → ℕ ∈ V) | 
| 5 |  | ltwenn 14004 | . . . . . . 7
⊢  < We
ℕ | 
| 6 | 5 | a1i 11 | . . . . . 6
⊢ (𝑔:ℕ–onto→𝐴 → < We ℕ) | 
| 7 | 2, 4, 6 | wessf1orn 45196 | . . . . 5
⊢ (𝑔:ℕ–onto→𝐴 → ∃𝑥 ∈ 𝒫 ℕ(𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) | 
| 8 |  | f1odm 6851 | . . . . . . . . . . 11
⊢ ((𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔 → dom (𝑔 ↾ 𝑥) = 𝑥) | 
| 9 | 8 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 ℕ ∧
(𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → dom (𝑔 ↾ 𝑥) = 𝑥) | 
| 10 |  | elpwi 4606 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 ℕ →
𝑥 ⊆
ℕ) | 
| 11 | 10 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 ℕ ∧
(𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → 𝑥 ⊆
ℕ) | 
| 12 | 9, 11 | eqsstrd 4017 | . . . . . . . . 9
⊢ ((𝑥 ∈ 𝒫 ℕ ∧
(𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → dom (𝑔 ↾ 𝑥) ⊆ ℕ) | 
| 13 | 12 | 3adant1 1130 | . . . . . . . 8
⊢ ((𝑔:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝒫 ℕ ∧ (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → dom (𝑔 ↾ 𝑥) ⊆ ℕ) | 
| 14 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑔:ℕ–onto→𝐴 ∧ (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) | 
| 15 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → (𝑔 ↾ 𝑥) = (𝑔 ↾ 𝑥)) | 
| 16 | 8 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ ((𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔 → 𝑥 = dom (𝑔 ↾ 𝑥)) | 
| 17 | 16 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → 𝑥 = dom (𝑔 ↾ 𝑥)) | 
| 18 |  | forn 6822 | . . . . . . . . . . . 12
⊢ (𝑔:ℕ–onto→𝐴 → ran 𝑔 = 𝐴) | 
| 19 | 18 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → ran 𝑔 = 𝐴) | 
| 20 | 15, 17, 19 | f1oeq123d 6841 | . . . . . . . . . 10
⊢ ((𝑔:ℕ–onto→𝐴 ∧ (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → ((𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔 ↔ (𝑔 ↾ 𝑥):dom (𝑔 ↾ 𝑥)–1-1-onto→𝐴)) | 
| 21 | 14, 20 | mpbid 232 | . . . . . . . . 9
⊢ ((𝑔:ℕ–onto→𝐴 ∧ (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → (𝑔 ↾ 𝑥):dom (𝑔 ↾ 𝑥)–1-1-onto→𝐴) | 
| 22 | 21 | 3adant2 1131 | . . . . . . . 8
⊢ ((𝑔:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝒫 ℕ ∧ (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → (𝑔 ↾ 𝑥):dom (𝑔 ↾ 𝑥)–1-1-onto→𝐴) | 
| 23 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑔 ∈ V | 
| 24 | 23 | resex 6046 | . . . . . . . . 9
⊢ (𝑔 ↾ 𝑥) ∈ V | 
| 25 |  | dmeq 5913 | . . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ↾ 𝑥) → dom 𝑓 = dom (𝑔 ↾ 𝑥)) | 
| 26 | 25 | sseq1d 4014 | . . . . . . . . . 10
⊢ (𝑓 = (𝑔 ↾ 𝑥) → (dom 𝑓 ⊆ ℕ ↔ dom (𝑔 ↾ 𝑥) ⊆ ℕ)) | 
| 27 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ↾ 𝑥) → 𝑓 = (𝑔 ↾ 𝑥)) | 
| 28 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ↾ 𝑥) → 𝐴 = 𝐴) | 
| 29 | 27, 25, 28 | f1oeq123d 6841 | . . . . . . . . . 10
⊢ (𝑓 = (𝑔 ↾ 𝑥) → (𝑓:dom 𝑓–1-1-onto→𝐴 ↔ (𝑔 ↾ 𝑥):dom (𝑔 ↾ 𝑥)–1-1-onto→𝐴)) | 
| 30 | 26, 29 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑓 = (𝑔 ↾ 𝑥) → ((dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴) ↔ (dom (𝑔 ↾ 𝑥) ⊆ ℕ ∧ (𝑔 ↾ 𝑥):dom (𝑔 ↾ 𝑥)–1-1-onto→𝐴))) | 
| 31 | 24, 30 | spcev 3605 | . . . . . . . 8
⊢ ((dom
(𝑔 ↾ 𝑥) ⊆ ℕ ∧ (𝑔 ↾ 𝑥):dom (𝑔 ↾ 𝑥)–1-1-onto→𝐴) → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴)) | 
| 32 | 13, 22, 31 | syl2anc 584 | . . . . . . 7
⊢ ((𝑔:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝒫 ℕ ∧ (𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔) → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴)) | 
| 33 | 32 | 3exp 1119 | . . . . . 6
⊢ (𝑔:ℕ–onto→𝐴 → (𝑥 ∈ 𝒫 ℕ → ((𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔 → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴)))) | 
| 34 | 33 | rexlimdv 3152 | . . . . 5
⊢ (𝑔:ℕ–onto→𝐴 → (∃𝑥 ∈ 𝒫 ℕ(𝑔 ↾ 𝑥):𝑥–1-1-onto→ran
𝑔 → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴))) | 
| 35 | 7, 34 | mpd 15 | . . . 4
⊢ (𝑔:ℕ–onto→𝐴 → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴)) | 
| 36 | 35 | a1i 11 | . . 3
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → (𝑔:ℕ–onto→𝐴 → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴))) | 
| 37 | 36 | exlimdv 1932 | . 2
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) →
(∃𝑔 𝑔:ℕ–onto→𝐴 → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴))) | 
| 38 | 1, 37 | mpd 15 | 1
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) →
∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴)) |