Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . 4
⊢
(2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V |
2 | | axcc2lem.3 |
. . . 4
⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd
‘(𝑓‘(𝐴‘𝑛)))) |
3 | 1, 2 | fnmpti 5935 |
. . 3
⊢ 𝐺 Fn ω |
4 | | snex 4835 |
. . . . . . . . . . . . . . 15
⊢ {𝑛} ∈ V |
5 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐾‘𝑛) ∈ V |
6 | 4, 5 | xpex 6860 |
. . . . . . . . . . . . . 14
⊢ ({𝑛} × (𝐾‘𝑛)) ∈ V |
7 | | axcc2lem.2 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) |
8 | 7 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ω ∧ ({𝑛} × (𝐾‘𝑛)) ∈ V) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛))) |
9 | 6, 8 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛))) |
10 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑛 ∈ V |
11 | 10 | snnz 4252 |
. . . . . . . . . . . . . 14
⊢ {𝑛} ≠ ∅ |
12 | | 0ex 4718 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ V |
13 | 12 | snnz 4252 |
. . . . . . . . . . . . . . . . 17
⊢ {∅}
≠ ∅ |
14 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = {∅}) |
15 | 14 | neeq1d 2841 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑛) = ∅ → (if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅ ↔ {∅} ≠
∅)) |
16 | 13, 15 | mpbiri 247 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅) |
17 | | iffalse 4045 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛)) |
18 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑛) ≠ ∅ ↔ ¬ (𝐹‘𝑛) = ∅) |
19 | 18 | biimpri 217 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ≠ ∅) |
20 | 17, 19 | eqnetrd 2849 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝐹‘𝑛) = ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅) |
21 | 16, 20 | pm2.61i 175 |
. . . . . . . . . . . . . . 15
⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅ |
22 | | p0ex 4779 |
. . . . . . . . . . . . . . . . . 18
⊢ {∅}
∈ V |
23 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹‘𝑛) ∈ V |
24 | 22, 23 | ifex 4106 |
. . . . . . . . . . . . . . . . 17
⊢ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V |
25 | | axcc2lem.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐾 = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) |
26 | 25 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ω ∧ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ∈ V) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) |
27 | 24, 26 | mpan2 703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) |
28 | 27 | neeq1d 2841 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → ((𝐾‘𝑛) ≠ ∅ ↔ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) ≠ ∅)) |
29 | 21, 28 | mpbiri 247 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → (𝐾‘𝑛) ≠ ∅) |
30 | | xpnz 5472 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) ↔ ({𝑛} × (𝐾‘𝑛)) ≠ ∅) |
31 | 30 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → ({𝑛} × (𝐾‘𝑛)) ≠ ∅) |
32 | 11, 29, 31 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ≠ ∅) |
33 | 9, 32 | eqnetrd 2849 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ≠ ∅) |
34 | 6, 7 | fnmpti 5935 |
. . . . . . . . . . . . . 14
⊢ 𝐴 Fn ω |
35 | | fnfvelrn 6264 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴‘𝑛) ∈ ran 𝐴) |
36 | 34, 35 | mpan 702 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → (𝐴‘𝑛) ∈ ran 𝐴) |
37 | | neeq1 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐴‘𝑛) → (𝑧 ≠ ∅ ↔ (𝐴‘𝑛) ≠ ∅)) |
38 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐴‘𝑛) → (𝑓‘𝑧) = (𝑓‘(𝐴‘𝑛))) |
39 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐴‘𝑛) → 𝑧 = (𝐴‘𝑛)) |
40 | 38, 39 | eleq12d 2682 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐴‘𝑛) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))) |
41 | 37, 40 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐴‘𝑛) → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))) |
42 | 41 | rspccv 3279 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ((𝐴‘𝑛) ∈ ran 𝐴 → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))) |
43 | 36, 42 | syl5 33 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐴‘𝑛) ≠ ∅ → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)))) |
44 | 33, 43 | mpdi 44 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛))) |
45 | 44 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛)) |
46 | 9 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ω → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)))) |
47 | 46 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝑓‘(𝐴‘𝑛)) ∈ (𝐴‘𝑛) ↔ (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)))) |
48 | 45, 47 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛))) |
49 | | xp2nd 7090 |
. . . . . . . . 9
⊢ ((𝑓‘(𝐴‘𝑛)) ∈ ({𝑛} × (𝐾‘𝑛)) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛)) |
50 | 48, 49 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → (2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛)) |
51 | 50 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2nd
‘(𝑓‘(𝐴‘𝑛))) ∈ (𝐾‘𝑛)) |
52 | 2 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ω ∧
(2nd ‘(𝑓‘(𝐴‘𝑛))) ∈ V) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛)))) |
53 | 1, 52 | mpan2 703 |
. . . . . . . . 9
⊢ (𝑛 ∈ ω → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛)))) |
54 | 53 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) = (2nd ‘(𝑓‘(𝐴‘𝑛)))) |
55 | 54 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (2nd
‘(𝑓‘(𝐴‘𝑛))) = (𝐺‘𝑛)) |
56 | 27 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) |
57 | | ifnefalse 4048 |
. . . . . . . . 9
⊢ ((𝐹‘𝑛) ≠ ∅ → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛)) |
58 | 57 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) = (𝐹‘𝑛)) |
59 | 56, 58 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐾‘𝑛) = (𝐹‘𝑛)) |
60 | 51, 55, 59 | 3eltr3d 2702 |
. . . . . 6
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ∧ (𝐹‘𝑛) ≠ ∅) → (𝐺‘𝑛) ∈ (𝐹‘𝑛)) |
61 | 60 | 3expia 1259 |
. . . . 5
⊢ ((𝑛 ∈ ω ∧
∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) |
62 | 61 | expcom 450 |
. . . 4
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → (𝑛 ∈ ω → ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))) |
63 | 62 | ralrimiv 2948 |
. . 3
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) |
64 | | omex 8423 |
. . . . 5
⊢ ω
∈ V |
65 | | fnex 6386 |
. . . . 5
⊢ ((𝐺 Fn ω ∧ ω ∈
V) → 𝐺 ∈
V) |
66 | 3, 64, 65 | mp2an 704 |
. . . 4
⊢ 𝐺 ∈ V |
67 | | fneq1 5893 |
. . . . 5
⊢ (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω)) |
68 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛)) |
69 | 68 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∈ (𝐹‘𝑛) ↔ (𝐺‘𝑛) ∈ (𝐹‘𝑛))) |
70 | 69 | imbi2d 329 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))) |
71 | 70 | ralbidv 2969 |
. . . . 5
⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)) ↔ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛)))) |
72 | 67, 71 | anbi12d 743 |
. . . 4
⊢ (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))))) |
73 | 66, 72 | spcev 3273 |
. . 3
⊢ ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝐺‘𝑛) ∈ (𝐹‘𝑛))) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))) |
74 | 3, 63, 73 | sylancr 694 |
. 2
⊢
(∀𝑧 ∈
ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛)))) |
75 | 6 | a1i 11 |
. . . . . 6
⊢ ((ω
∈ V ∧ 𝑛 ∈
ω) → ({𝑛}
× (𝐾‘𝑛)) ∈ V) |
76 | 75, 7 | fmptd 6292 |
. . . . 5
⊢ (ω
∈ V → 𝐴:ω⟶V) |
77 | 64, 76 | ax-mp 5 |
. . . 4
⊢ 𝐴:ω⟶V |
78 | | sneq 4135 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘}) |
79 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝐾‘𝑛) = (𝐾‘𝑘)) |
80 | 78, 79 | xpeq12d 5064 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘))) |
81 | 80, 7, 6 | fvmpt3i 6196 |
. . . . . . . 8
⊢ (𝑘 ∈ ω → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘))) |
82 | 81 | adantl 481 |
. . . . . . 7
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑘) = ({𝑘} × (𝐾‘𝑘))) |
83 | 82 | eqeq2d 2620 |
. . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) ↔ (𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)))) |
84 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (𝐴‘𝑛) = ({𝑛} × (𝐾‘𝑛))) |
85 | 84 | eqeq1d 2612 |
. . . . . . 7
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)))) |
86 | | xp11 5488 |
. . . . . . . . . 10
⊢ (({𝑛} ≠ ∅ ∧ (𝐾‘𝑛) ≠ ∅) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)))) |
87 | 11, 29, 86 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)))) |
88 | 10 | sneqr 4311 |
. . . . . . . . . 10
⊢ ({𝑛} = {𝑘} → 𝑛 = 𝑘) |
89 | 88 | adantr 480 |
. . . . . . . . 9
⊢ (({𝑛} = {𝑘} ∧ (𝐾‘𝑛) = (𝐾‘𝑘)) → 𝑛 = 𝑘) |
90 | 87, 89 | syl6bi 242 |
. . . . . . . 8
⊢ (𝑛 ∈ ω → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘)) |
91 | 90 | adantr 480 |
. . . . . . 7
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → (({𝑛} × (𝐾‘𝑛)) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘)) |
92 | 85, 91 | sylbid 229 |
. . . . . 6
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = ({𝑘} × (𝐾‘𝑘)) → 𝑛 = 𝑘)) |
93 | 83, 92 | sylbid 229 |
. . . . 5
⊢ ((𝑛 ∈ ω ∧ 𝑘 ∈ ω) → ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘)) |
94 | 93 | rgen2a 2960 |
. . . 4
⊢
∀𝑛 ∈
ω ∀𝑘 ∈
ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘) |
95 | | dff13 6416 |
. . . 4
⊢ (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴‘𝑛) = (𝐴‘𝑘) → 𝑛 = 𝑘))) |
96 | 77, 94, 95 | mpbir2an 957 |
. . 3
⊢ 𝐴:ω–1-1→V |
97 | | f1f1orn 6061 |
. . . 4
⊢ (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran
𝐴) |
98 | 64 | f1oen 7862 |
. . . 4
⊢ (𝐴:ω–1-1-onto→ran
𝐴 → ω ≈
ran 𝐴) |
99 | | ensym 7891 |
. . . 4
⊢ (ω
≈ ran 𝐴 → ran
𝐴 ≈
ω) |
100 | 97, 98, 99 | 3syl 18 |
. . 3
⊢ (𝐴:ω–1-1→V → ran 𝐴 ≈ ω) |
101 | 7 | rneqi 5273 |
. . . . 5
⊢ ran 𝐴 = ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) |
102 | | dmmptg 5549 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ω ({𝑛} × (𝐾‘𝑛)) ∈ V → dom (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) = ω) |
103 | 6 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ω → ({𝑛} × (𝐾‘𝑛)) ∈ V) |
104 | 102, 103 | mprg 2910 |
. . . . . . 7
⊢ dom
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) = ω |
105 | 104, 64 | eqeltri 2684 |
. . . . . 6
⊢ dom
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) ∈ V |
106 | | funmpt 5840 |
. . . . . 6
⊢ Fun
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) |
107 | | funrnex 7026 |
. . . . . 6
⊢ (dom
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) ∈ V → (Fun (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) → ran (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) ∈ V)) |
108 | 105, 106,
107 | mp2 9 |
. . . . 5
⊢ ran
(𝑛 ∈ ω ↦
({𝑛} × (𝐾‘𝑛))) ∈ V |
109 | 101, 108 | eqeltri 2684 |
. . . 4
⊢ ran 𝐴 ∈ V |
110 | | breq1 4586 |
. . . . 5
⊢ (𝑎 = ran 𝐴 → (𝑎 ≈ ω ↔ ran 𝐴 ≈ ω)) |
111 | | raleq 3115 |
. . . . . 6
⊢ (𝑎 = ran 𝐴 → (∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
112 | 111 | exbidv 1837 |
. . . . 5
⊢ (𝑎 = ran 𝐴 → (∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
113 | 110, 112 | imbi12d 333 |
. . . 4
⊢ (𝑎 = ran 𝐴 → ((𝑎 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ↔ (ran 𝐴 ≈ ω → ∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))) |
114 | | ax-cc 9140 |
. . . 4
⊢ (𝑎 ≈ ω →
∃𝑓∀𝑧 ∈ 𝑎 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
115 | 109, 113,
114 | vtocl 3232 |
. . 3
⊢ (ran
𝐴 ≈ ω →
∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
116 | 96, 100, 115 | mp2b 10 |
. 2
⊢
∃𝑓∀𝑧 ∈ ran 𝐴(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) |
117 | 74, 116 | exlimiiv 1846 |
1
⊢
∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) |