Step | Hyp | Ref
| Expression |
1 | | f1oi 5480 |
. . . . . . . . . . 11
⊢ ( I
↾ 𝐴):𝐴–1-1-onto→𝐴 |
2 | | f1of 5442 |
. . . . . . . . . . 11
⊢ (( I
↾ 𝐴):𝐴–1-1-onto→𝐴 → ( I ↾ 𝐴):𝐴⟶𝐴) |
3 | 1, 2 | mp1i 10 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → ( I ↾
𝐴):𝐴⟶𝐴) |
4 | | fconst6g 5396 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (1o × {𝑥}):1o⟶𝐴) |
5 | 4 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) →
(1o × {𝑥}):1o⟶𝐴) |
6 | 3, 5 | casef 7065 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → case(( I
↾ 𝐴), (1o
× {𝑥})):(𝐴 ⊔
1o)⟶𝐴) |
7 | | ffun 5350 |
. . . . . . . . 9
⊢ (case(( I
↾ 𝐴), (1o
× {𝑥})):(𝐴 ⊔
1o)⟶𝐴
→ Fun case(( I ↾ 𝐴), (1o × {𝑥}))) |
8 | 6, 7 | syl 14 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → Fun case((
I ↾ 𝐴),
(1o × {𝑥}))) |
9 | | vex 2733 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
10 | 9 | a1i 9 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → 𝑓 ∈ V) |
11 | | cofunexg 6088 |
. . . . . . . 8
⊢ ((Fun
case(( I ↾ 𝐴),
(1o × {𝑥})) ∧ 𝑓 ∈ V) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓) ∈ V) |
12 | 8, 10, 11 | syl2anc 409 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → (case(( I
↾ 𝐴), (1o
× {𝑥})) ∘ 𝑓) ∈ V) |
13 | | fof 5420 |
. . . . . . . . . 10
⊢ (𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝑓:ω⟶(𝐴 ⊔
1o)) |
14 | 13 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → 𝑓:ω⟶(𝐴 ⊔
1o)) |
15 | | fco 5363 |
. . . . . . . . 9
⊢ ((case((
I ↾ 𝐴),
(1o × {𝑥})):(𝐴 ⊔ 1o)⟶𝐴 ∧ 𝑓:ω⟶(𝐴 ⊔ 1o)) → (case(( I
↾ 𝐴), (1o
× {𝑥})) ∘ 𝑓):ω⟶𝐴) |
16 | 6, 14, 15 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → (case(( I
↾ 𝐴), (1o
× {𝑥})) ∘ 𝑓):ω⟶𝐴) |
17 | | simplr 525 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) → 𝑓:ω–onto→(𝐴 ⊔ 1o)) |
18 | | djulcl 7028 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐴 → (inl‘𝑦) ∈ (𝐴 ⊔ 1o)) |
19 | 18 | adantl 275 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) → (inl‘𝑦) ∈ (𝐴 ⊔ 1o)) |
20 | | foelrn 5732 |
. . . . . . . . . . 11
⊢ ((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧
(inl‘𝑦) ∈ (𝐴 ⊔ 1o)) →
∃𝑧 ∈ ω
(inl‘𝑦) = (𝑓‘𝑧)) |
21 | 17, 19, 20 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) → ∃𝑧 ∈ ω (inl‘𝑦) = (𝑓‘𝑧)) |
22 | | fofn 5422 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝑓 Fn ω) |
23 | 22 | ad4antlr 492 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → 𝑓 Fn ω) |
24 | | simplr 525 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → 𝑧 ∈ ω) |
25 | | fvco2 5565 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 Fn ω ∧ 𝑧 ∈ ω) → ((case((
I ↾ 𝐴),
(1o × {𝑥})) ∘ 𝑓)‘𝑧) = (case(( I ↾ 𝐴), (1o × {𝑥}))‘(𝑓‘𝑧))) |
26 | 23, 24, 25 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧) = (case(( I ↾ 𝐴), (1o × {𝑥}))‘(𝑓‘𝑧))) |
27 | | simpr 109 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → (inl‘𝑦) = (𝑓‘𝑧)) |
28 | 27 | fveq2d 5500 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → (case(( I ↾ 𝐴), (1o × {𝑥}))‘(inl‘𝑦)) = (case(( I ↾ 𝐴), (1o × {𝑥}))‘(𝑓‘𝑧))) |
29 | | fnresi 5315 |
. . . . . . . . . . . . . . . 16
⊢ ( I
↾ 𝐴) Fn 𝐴 |
30 | 29 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → ( I ↾ 𝐴) Fn 𝐴) |
31 | | vex 2733 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
32 | 31 | fconst6 5397 |
. . . . . . . . . . . . . . . 16
⊢
(1o × {𝑥}):1o⟶V |
33 | | ffun 5350 |
. . . . . . . . . . . . . . . 16
⊢
((1o × {𝑥}):1o⟶V → Fun
(1o × {𝑥})) |
34 | 32, 33 | mp1i 10 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → Fun (1o × {𝑥})) |
35 | | simpllr 529 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → 𝑦 ∈ 𝐴) |
36 | 30, 34, 35 | caseinl 7068 |
. . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → (case(( I ↾ 𝐴), (1o × {𝑥}))‘(inl‘𝑦)) = (( I ↾ 𝐴)‘𝑦)) |
37 | 26, 28, 36 | 3eqtr2d 2209 |
. . . . . . . . . . . . 13
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧) = (( I ↾ 𝐴)‘𝑦)) |
38 | | fvresi 5689 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐴 → (( I ↾ 𝐴)‘𝑦) = 𝑦) |
39 | 35, 38 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → (( I ↾ 𝐴)‘𝑦) = 𝑦) |
40 | 37, 39 | eqtr2d 2204 |
. . . . . . . . . . . 12
⊢
(((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓‘𝑧)) → 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧)) |
41 | 40 | ex 114 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ ω) → ((inl‘𝑦) = (𝑓‘𝑧) → 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧))) |
42 | 41 | reximdva 2572 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) → (∃𝑧 ∈ ω (inl‘𝑦) = (𝑓‘𝑧) → ∃𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧))) |
43 | 21, 42 | mpd 13 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦 ∈ 𝐴) → ∃𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧)) |
44 | 43 | ralrimiva 2543 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) →
∀𝑦 ∈ 𝐴 ∃𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧)) |
45 | | dffo3 5643 |
. . . . . . . 8
⊢ ((case((
I ↾ 𝐴),
(1o × {𝑥})) ∘ 𝑓):ω–onto→𝐴 ↔ ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω⟶𝐴 ∧ ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧))) |
46 | 16, 44, 45 | sylanbrc 415 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → (case(( I
↾ 𝐴), (1o
× {𝑥})) ∘ 𝑓):ω–onto→𝐴) |
47 | | foeq1 5416 |
. . . . . . . 8
⊢ (𝑔 = (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓) → (𝑔:ω–onto→𝐴 ↔ (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω–onto→𝐴)) |
48 | 47 | spcegv 2818 |
. . . . . . 7
⊢ ((case((
I ↾ 𝐴),
(1o × {𝑥})) ∘ 𝑓) ∈ V → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω–onto→𝐴 → ∃𝑔 𝑔:ω–onto→𝐴)) |
49 | 12, 46, 48 | sylc 62 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) →
∃𝑔 𝑔:ω–onto→𝐴) |
50 | 49 | ex 114 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → (𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→𝐴)) |
51 | 50 | exlimiv 1591 |
. . . 4
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→𝐴)) |
52 | 51 | exlimdv 1812 |
. . 3
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→𝐴)) |
53 | | foeq1 5416 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝑓:ω–onto→𝐴 ↔ 𝑔:ω–onto→𝐴)) |
54 | 53 | cbvexv 1911 |
. . 3
⊢
(∃𝑓 𝑓:ω–onto→𝐴 ↔ ∃𝑔 𝑔:ω–onto→𝐴) |
55 | 52, 54 | syl6ibr 161 |
. 2
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑓 𝑓:ω–onto→𝐴)) |
56 | | ctmlemr 7085 |
. 2
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))) |
57 | 55, 56 | impbid 128 |
1
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑓 𝑓:ω–onto→𝐴)) |