| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fvex 6919 | . . . 4
⊢
(2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V | 
| 2 |  | axcc2lem.3 | . . . 4
⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd
‘(𝑓‘(𝐴‘𝑛)))) | 
| 3 | 1, 2 | fnmpti 6711 | . . 3
⊢ 𝐺 Fn ω | 
| 4 |  | vsnex 5434 | . . . . . . . . . . . . . . 15
⊢ {𝑛} ∈ V | 
| 5 |  | fvex 6919 | . . . . . . . . . . . . . . 15
⊢ (𝐾‘𝑛) ∈ V | 
| 6 | 4, 5 | xpex 7773 | . . . . . . . . . . . . . 14
⊢ ({𝑛} × (𝐾‘𝑛)) ∈ V | 
| 7 |  | axcc2lem.2 | . . . . . . . . . . . . . . 15
⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) | 
| 8 | 7 | fvmpt2 7027 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐾‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛))) | 
| 9 | 6, 8 | mpan2 691 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛))) | 
| 10 |  | vex 3484 | . . . . . . . . . . . . . . 15
⊢ 𝑛 ∈ V | 
| 11 | 10 | snnz 4776 | . . . . . . . . . . . . . 14
⊢ {𝑛} ≠ ∅ | 
| 12 |  | 0ex 5307 | . . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ V | 
| 13 | 12 | snnz 4776 | . . . . . . . . . . . . . . . . 17
⊢ {∅}
≠ ∅ | 
| 14 |  | iftrue 4531 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = {∅}) | 
| 15 | 14 | neeq1d 3000 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑛) = ∅ → (if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅ ↔ {∅} ≠
∅)) | 
| 16 | 13, 15 | mpbiri 258 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅) | 
| 17 |  | iffalse 4534 | . . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛)) | 
| 18 |  | neqne 2948 | . . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ≠ ∅) | 
| 19 | 17, 18 | eqnetrd 3008 | . . . . . . . . . . . . . . . 16
⊢ (¬
(𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅) | 
| 20 | 16, 19 | pm2.61i 182 | . . . . . . . . . . . . . . 15
⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅ | 
| 21 |  | p0ex 5384 | . . . . . . . . . . . . . . . . . 18
⊢ {∅}
∈ V | 
| 22 |  | fvex 6919 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐹‘𝑛) ∈ V | 
| 23 | 21, 22 | ifex 4576 | . . . . . . . . . . . . . . . . 17
⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V | 
| 24 |  | axcc2lem.1 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐾 = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) | 
| 25 | 24 | fvmpt2 7027 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ω ∧ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) | 
| 26 | 23, 25 | mpan2 691 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) | 
| 27 | 26 | neeq1d 3000 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → ((𝐾‘𝑛) ≠ ∅ ↔ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)) | 
| 28 | 20, 27 | mpbiri 258 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → (𝐾‘𝑛) ≠ ∅) | 
| 29 |  | xpnz 6179 | . . . . . . . . . . . . . . 15
⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) ↔ ({𝑛} × (𝐾‘𝑛)) ≠ ∅) | 
| 30 | 29 | biimpi 216 | . . . . . . . . . . . . . 14
⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → ({𝑛} × (𝐾‘𝑛)) ≠ ∅) | 
| 31 | 11, 28, 30 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ≠ ∅) | 
| 32 | 9, 31 | eqnetrd 3008 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ≠ ∅) | 
| 33 | 6, 7 | fnmpti 6711 | . . . . . . . . . . . . . 14
⊢ 𝐴 Fn ω | 
| 34 |  | fnfvelrn 7100 | . . . . . . . . . . . . . 14
⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴) | 
| 35 | 33, 34 | mpan 690 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ∈ ran 𝐴) | 
| 36 |  | neeq1 3003 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐴‘𝑛) → (𝑧 ≠ ∅ ↔ (𝐴‘𝑛) ≠ ∅)) | 
| 37 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛))) | 
| 38 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛)) | 
| 39 | 37, 38 | eleq12d 2835 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))) | 
| 40 | 36, 39 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐴‘𝑛) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))) | 
| 41 | 40 | rspccv 3619 | . . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝐴‘𝑛) ∈ ran 𝐴 → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))) | 
| 42 | 35, 41 | syl5 34 | . . . . . . . . . . . 12
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))) | 
| 43 | 32, 42 | mpdi 45 | . . . . . . . . . . 11
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))) | 
| 44 | 43 | impcom 407 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)) | 
| 45 | 9 | eleq2d 2827 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ω → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)))) | 
| 46 | 45 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)))) | 
| 47 | 44, 46 | mpbid 232 | . . . . . . . . 9
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))) | 
| 48 |  | xp2nd 8047 | . . . . . . . . 9
⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛)) | 
| 49 | 47, 48 | syl 17 | . . . . . . . 8
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛)) | 
| 50 | 49 | 3adant3 1133 | . . . . . . 7
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2nd
‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛)) | 
| 51 | 2 | fvmpt2 7027 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ω ∧
(2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛)))) | 
| 52 | 1, 51 | mpan2 691 | . . . . . . . . 9
⊢ (𝑛 ∈ ω → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛)))) | 
| 53 | 52 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛)))) | 
| 54 | 53 | eqcomd 2743 | . . . . . . 7
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2nd
‘(𝑓‘(𝐴‘𝑛))) = (𝐺‘𝑛)) | 
| 55 | 26 | 3ad2ant1 1134 | . . . . . . . 8
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) | 
| 56 |  | ifnefalse 4537 | . . . . . . . . 9
⊢ ((𝐹‘𝑛) ≠ ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛)) | 
| 57 | 56 | 3ad2ant3 1136 | . . . . . . . 8
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛)) | 
| 58 | 55, 57 | eqtrd 2777 | . . . . . . 7
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = (𝐹‘𝑛)) | 
| 59 | 50, 54, 58 | 3eltr3d 2855 | . . . . . 6
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) ∈ (𝐹‘𝑛)) | 
| 60 | 59 | 3expia 1122 | . . . . 5
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) | 
| 61 | 60 | expcom 413 | . . . 4
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))) | 
| 62 | 61 | ralrimiv 3145 | . . 3
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) | 
| 63 |  | omex 9683 | . . . . 5
⊢ ω
∈ V | 
| 64 |  | fnex 7237 | . . . . 5
⊢ ((𝐺 Fn ω ∧ ω ∈
V) → 𝐺 ∈
V) | 
| 65 | 3, 63, 64 | mp2an 692 | . . . 4
⊢ 𝐺 ∈ V | 
| 66 |  | fneq1 6659 | . . . . 5
⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω)) | 
| 67 |  | fveq1 6905 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛)) | 
| 68 | 67 | eleq1d 2826 | . . . . . . 7
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛))) | 
| 69 | 68 | imbi2d 340 | . . . . . 6
⊢ (𝑔 = 𝐺 → (((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))) | 
| 70 | 69 | ralbidv 3178 | . . . . 5
⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))) | 
| 71 | 66, 70 | anbi12d 632 | . . . 4
⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))) | 
| 72 | 65, 71 | spcev 3606 | . . 3
⊢ ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))) | 
| 73 | 3, 62, 72 | sylancr 587 | . 2
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))) | 
| 74 | 6 | a1i 11 | . . . . . 6
⊢ ((ω
∈ V ∧ 𝑛 ∈
ω) → ({𝑛}
× (𝐾‘𝑛)) ∈ V) | 
| 75 | 74, 7 | fmptd 7134 | . . . . 5
⊢ (ω
∈ V → 𝐴:ω⟶V) | 
| 76 | 63, 75 | ax-mp 5 | . . . 4
⊢ 𝐴:ω⟶V | 
| 77 |  | sneq 4636 | . . . . . . . . . 10
⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘}) | 
| 78 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝐾‘𝑛) = (𝐾‘𝑘)) | 
| 79 | 77, 78 | xpeq12d 5716 | . . . . . . . . 9
⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘))) | 
| 80 | 79, 7, 6 | fvmpt3i 7021 | . . . . . . . 8
⊢ (𝑘 ∈ ω → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘))) | 
| 81 | 80 | adantl 481 | . . . . . . 7
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘))) | 
| 82 | 81 | eqeq2d 2748 | . . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)))) | 
| 83 | 9 | adantr 480 | . . . . . . . 8
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛))) | 
| 84 | 83 | eqeq1d 2739 | . . . . . . 7
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)))) | 
| 85 |  | xp11 6195 | . . . . . . . . . 10
⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)))) | 
| 86 | 11, 28, 85 | sylancr 587 | . . . . . . . . 9
⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)))) | 
| 87 | 10 | sneqr 4840 | . . . . . . . . . 10
⊢ ({𝑛} = {𝑘} → 𝑛 = 𝑘) | 
| 88 | 87 | adantr 480 | . . . . . . . . 9
⊢ (({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)) → 𝑛 = 𝑘) | 
| 89 | 86, 88 | biimtrdi 253 | . . . . . . . 8
⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘)) | 
| 90 | 89 | adantr 480 | . . . . . . 7
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘)) | 
| 91 | 84, 90 | sylbid 240 | . . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘)) | 
| 92 | 82, 91 | sylbid 240 | . . . . 5
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)) | 
| 93 | 92 | rgen2 3199 | . . . 4
⊢
∀𝑛 ∈
ω ∀𝑘 ∈
ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘) | 
| 94 |  | dff13 7275 | . . . 4
⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))) | 
| 95 | 76, 93, 94 | mpbir2an 711 | . . 3
⊢ 𝐴:ω–1-1→V | 
| 96 |  | f1f1orn 6859 | . . . 4
⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran
𝐴) | 
| 97 | 63 | f1oen 9013 | . . . 4
⊢ (𝐴:ω–1-1-onto→ran
𝐴 → ω ≈
ran 𝐴) | 
| 98 |  | ensym 9043 | . . . 4
⊢ (ω
≈ ran 𝐴 → ran
𝐴 ≈
ω) | 
| 99 | 96, 97, 98 | 3syl 18 | . . 3
⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω) | 
| 100 | 7 | rneqi 5948 | . . . . 5
⊢ ran 𝐴 = ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) | 
| 101 |  | dmmptg 6262 | . . . . . . . 8
⊢
(∀𝑛 ∈
ω ({𝑛} × (𝐾‘𝑛)) ∈ V → dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω) | 
| 102 | 6 | a1i 11 | . . . . . . . 8
⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ∈ V) | 
| 103 | 101, 102 | mprg 3067 | . . . . . . 7
⊢ dom
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) = ω | 
| 104 | 103, 63 | eqeltri 2837 | . . . . . 6
⊢ dom
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) ∈ V | 
| 105 |  | funmpt 6604 | . . . . . 6
⊢ Fun
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) | 
| 106 |  | funrnex 7978 | . . . . . 6
⊢ (dom
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) ∈ V → (Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) → ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V)) | 
| 107 | 104, 105,
106 | mp2 9 | . . . . 5
⊢ ran
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) ∈ V | 
| 108 | 100, 107 | eqeltri 2837 | . . . 4
⊢ ran 𝐴 ∈ V | 
| 109 |  | breq1 5146 | . . . . 5
⊢ (𝑎 = ran 𝐴 → (𝑎 ≈ ω ↔ ran 𝐴 ≈ ω)) | 
| 110 |  | raleq 3323 | . . . . . 6
⊢ (𝑎 = ran 𝐴 → (∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) | 
| 111 | 110 | exbidv 1921 | . . . . 5
⊢ (𝑎 = ran 𝐴 → (∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) | 
| 112 | 109, 111 | imbi12d 344 | . . . 4
⊢ (𝑎 = ran 𝐴 → ((𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))) | 
| 113 |  | ax-cc 10475 | . . . 4
⊢ (𝑎 ≈ ω →
∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) | 
| 114 | 108, 112,
113 | vtocl 3558 | . . 3
⊢ (ran
𝐴 ≈ ω →
∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) | 
| 115 | 95, 99, 114 | mp2b 10 | . 2
⊢
∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) | 
| 116 | 73, 115 | exlimiiv 1931 | 1
⊢
∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) |