Step | Hyp | Ref
| Expression |
1 | | brdomi 7966 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
2 | | neq0 3930 |
. . . . 5
⊢ (¬
𝐴 = ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
3 | | simpl3 1066 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → 𝑋 ∈ AC 𝐵) |
4 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴) → 𝑔:𝐴⟶(𝒫 𝑋 ∖ {∅})) |
5 | 4 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝑔:𝐴⟶(𝒫 𝑋 ∖ {∅})) |
6 | | simpll1 1100 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑦 ∈ 𝐵) → 𝑓:𝐴–1-1→𝐵) |
7 | | f1f1orn 6148 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐴–1-1→𝐵 → 𝑓:𝐴–1-1-onto→ran
𝑓) |
8 | | f1ocnv 6149 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐴–1-1-onto→ran
𝑓 → ◡𝑓:ran 𝑓–1-1-onto→𝐴) |
9 | | f1of 6137 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑓:ran 𝑓–1-1-onto→𝐴 → ◡𝑓:ran 𝑓⟶𝐴) |
10 | 6, 7, 8, 9 | 4syl 19 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑦 ∈ 𝐵) → ◡𝑓:ran 𝑓⟶𝐴) |
11 | 10 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ ran 𝑓) → (◡𝑓‘𝑦) ∈ 𝐴) |
12 | | simpl2 1065 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → 𝑥 ∈ 𝐴) |
13 | 12 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑦 ∈ 𝐵) ∧ ¬ 𝑦 ∈ ran 𝑓) → 𝑥 ∈ 𝐴) |
14 | 11, 13 | ifclda 4120 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑦 ∈ 𝐵) → if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥) ∈ 𝐴) |
15 | 5, 14 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑦 ∈ 𝐵) → (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ∈ (𝒫 𝑋 ∖ {∅})) |
16 | | eldifsn 4317 |
. . . . . . . . . . . . . 14
⊢ ((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ∈ (𝒫 𝑋 ∖ {∅}) ↔ ((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ∈ 𝒫 𝑋 ∧ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ≠ ∅)) |
17 | | elpwi 4168 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ∈ 𝒫 𝑋 → (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ⊆ 𝑋) |
18 | 17 | anim1i 592 |
. . . . . . . . . . . . . 14
⊢ (((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ∈ 𝒫 𝑋 ∧ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ≠ ∅) → ((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ⊆ 𝑋 ∧ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ≠ ∅)) |
19 | 16, 18 | sylbi 207 |
. . . . . . . . . . . . 13
⊢ ((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ∈ (𝒫 𝑋 ∖ {∅}) → ((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ⊆ 𝑋 ∧ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ≠ ∅)) |
20 | 15, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑦 ∈ 𝐵) → ((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ⊆ 𝑋 ∧ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ≠ ∅)) |
21 | 20 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ∀𝑦 ∈ 𝐵 ((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ⊆ 𝑋 ∧ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ≠ ∅)) |
22 | | acni2 8869 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ AC 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ⊆ 𝑋 ∧ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ≠ ∅)) → ∃𝑘(𝑘:𝐵⟶𝑋 ∧ ∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)))) |
23 | 3, 21, 22 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ∃𝑘(𝑘:𝐵⟶𝑋 ∧ ∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)))) |
24 | | f1dm 6105 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–1-1→𝐵 → dom 𝑓 = 𝐴) |
25 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
26 | 25 | dmex 7099 |
. . . . . . . . . . . . . 14
⊢ dom 𝑓 ∈ V |
27 | 24, 26 | syl6eqelr 2710 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–1-1→𝐵 → 𝐴 ∈ V) |
28 | 27 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) → 𝐴 ∈ V) |
29 | 28 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ (𝑘:𝐵⟶𝑋 ∧ ∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)))) → 𝐴 ∈ V) |
30 | | simpll1 1100 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) → 𝑓:𝐴–1-1→𝐵) |
31 | | f1f 6101 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝐴–1-1→𝐵 → 𝑓:𝐴⟶𝐵) |
32 | | frn 6053 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ⊆ 𝐵) |
33 | | ssralv 3666 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑓 ⊆ 𝐵 → (∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) → ∀𝑦 ∈ ran 𝑓(𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)))) |
34 | 30, 31, 32, 33 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) → (∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) → ∀𝑦 ∈ ran 𝑓(𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)))) |
35 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ran 𝑓 → if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥) = (◡𝑓‘𝑦)) |
36 | 35 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ran 𝑓 → (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) = (𝑔‘(◡𝑓‘𝑦))) |
37 | 36 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ran 𝑓 → ((𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ↔ (𝑘‘𝑦) ∈ (𝑔‘(◡𝑓‘𝑦)))) |
38 | 37 | ralbiia 2979 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑦 ∈
ran 𝑓(𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) ↔ ∀𝑦 ∈ ran 𝑓(𝑘‘𝑦) ∈ (𝑔‘(◡𝑓‘𝑦))) |
39 | 34, 38 | syl6ib 241 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) → (∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) → ∀𝑦 ∈ ran 𝑓(𝑘‘𝑦) ∈ (𝑔‘(◡𝑓‘𝑦)))) |
40 | | f1fn 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–1-1→𝐵 → 𝑓 Fn 𝐴) |
41 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑓‘𝑧) → (𝑘‘𝑦) = (𝑘‘(𝑓‘𝑧))) |
42 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑓‘𝑧) → (◡𝑓‘𝑦) = (◡𝑓‘(𝑓‘𝑧))) |
43 | 42 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑓‘𝑧) → (𝑔‘(◡𝑓‘𝑦)) = (𝑔‘(◡𝑓‘(𝑓‘𝑧)))) |
44 | 41, 43 | eleq12d 2695 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑓‘𝑧) → ((𝑘‘𝑦) ∈ (𝑔‘(◡𝑓‘𝑦)) ↔ (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘(◡𝑓‘(𝑓‘𝑧))))) |
45 | 44 | ralrn 6362 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 Fn 𝐴 → (∀𝑦 ∈ ran 𝑓(𝑘‘𝑦) ∈ (𝑔‘(◡𝑓‘𝑦)) ↔ ∀𝑧 ∈ 𝐴 (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘(◡𝑓‘(𝑓‘𝑧))))) |
46 | 30, 40, 45 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) → (∀𝑦 ∈ ran 𝑓(𝑘‘𝑦) ∈ (𝑔‘(◡𝑓‘𝑦)) ↔ ∀𝑧 ∈ 𝐴 (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘(◡𝑓‘(𝑓‘𝑧))))) |
47 | 39, 46 | sylibd 229 |
. . . . . . . . . . . . 13
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) → (∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) → ∀𝑧 ∈ 𝐴 (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘(◡𝑓‘(𝑓‘𝑧))))) |
48 | 30, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) → 𝑓:𝐴–1-1-onto→ran
𝑓) |
49 | | f1ocnvfv1 6532 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:𝐴–1-1-onto→ran
𝑓 ∧ 𝑧 ∈ 𝐴) → (◡𝑓‘(𝑓‘𝑧)) = 𝑧) |
50 | 48, 49 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) ∧ 𝑧 ∈ 𝐴) → (◡𝑓‘(𝑓‘𝑧)) = 𝑧) |
51 | 50 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) ∧ 𝑧 ∈ 𝐴) → (𝑔‘(◡𝑓‘(𝑓‘𝑧))) = (𝑔‘𝑧)) |
52 | 51 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢
(((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) ∧ 𝑧 ∈ 𝐴) → ((𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘(◡𝑓‘(𝑓‘𝑧))) ↔ (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘𝑧))) |
53 | 52 | ralbidva 2985 |
. . . . . . . . . . . . 13
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) → (∀𝑧 ∈ 𝐴 (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘(◡𝑓‘(𝑓‘𝑧))) ↔ ∀𝑧 ∈ 𝐴 (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘𝑧))) |
54 | 47, 53 | sylibd 229 |
. . . . . . . . . . . 12
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ 𝑘:𝐵⟶𝑋) → (∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)) → ∀𝑧 ∈ 𝐴 (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘𝑧))) |
55 | 54 | impr 649 |
. . . . . . . . . . 11
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ (𝑘:𝐵⟶𝑋 ∧ ∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)))) → ∀𝑧 ∈ 𝐴 (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘𝑧)) |
56 | | acnlem 8871 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ ∀𝑧 ∈ 𝐴 (𝑘‘(𝑓‘𝑧)) ∈ (𝑔‘𝑧)) → ∃ℎ∀𝑧 ∈ 𝐴 (ℎ‘𝑧) ∈ (𝑔‘𝑧)) |
57 | 29, 55, 56 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ (𝑘:𝐵⟶𝑋 ∧ ∀𝑦 ∈ 𝐵 (𝑘‘𝑦) ∈ (𝑔‘if(𝑦 ∈ ran 𝑓, (◡𝑓‘𝑦), 𝑥)))) → ∃ℎ∀𝑧 ∈ 𝐴 (ℎ‘𝑧) ∈ (𝑔‘𝑧)) |
58 | 23, 57 | exlimddv 1863 |
. . . . . . . . 9
⊢ (((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) ∧ 𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ∃ℎ∀𝑧 ∈ 𝐴 (ℎ‘𝑧) ∈ (𝑔‘𝑧)) |
59 | 58 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) → ∀𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)∃ℎ∀𝑧 ∈ 𝐴 (ℎ‘𝑧) ∈ (𝑔‘𝑧)) |
60 | | elex 3212 |
. . . . . . . . . 10
⊢ (𝑋 ∈ AC 𝐵 → 𝑋 ∈ V) |
61 | | isacn 8867 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ 𝐴 ∈ V) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)∃ℎ∀𝑧 ∈ 𝐴 (ℎ‘𝑧) ∈ (𝑔‘𝑧))) |
62 | 60, 27, 61 | syl2anr 495 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑋 ∈ AC 𝐵) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)∃ℎ∀𝑧 ∈ 𝐴 (ℎ‘𝑧) ∈ (𝑔‘𝑧))) |
63 | 62 | 3adant2 1080 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑔 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)∃ℎ∀𝑧 ∈ 𝐴 (ℎ‘𝑧) ∈ (𝑔‘𝑧))) |
64 | 59, 63 | mpbird 247 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵) → 𝑋 ∈ AC 𝐴) |
65 | 64 | 3exp 1264 |
. . . . . 6
⊢ (𝑓:𝐴–1-1→𝐵 → (𝑥 ∈ 𝐴 → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴))) |
66 | 65 | exlimdv 1861 |
. . . . 5
⊢ (𝑓:𝐴–1-1→𝐵 → (∃𝑥 𝑥 ∈ 𝐴 → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴))) |
67 | 2, 66 | syl5bi 232 |
. . . 4
⊢ (𝑓:𝐴–1-1→𝐵 → (¬ 𝐴 = ∅ → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴))) |
68 | | acneq 8866 |
. . . . . . 7
⊢ (𝐴 = ∅ → AC
𝐴 = AC
∅) |
69 | | 0fin 8188 |
. . . . . . . 8
⊢ ∅
∈ Fin |
70 | | finacn 8873 |
. . . . . . . 8
⊢ (∅
∈ Fin → AC ∅ = V) |
71 | 69, 70 | ax-mp 5 |
. . . . . . 7
⊢ AC
∅ = V |
72 | 68, 71 | syl6eq 2672 |
. . . . . 6
⊢ (𝐴 = ∅ → AC
𝐴 = V) |
73 | 72 | eleq2d 2687 |
. . . . 5
⊢ (𝐴 = ∅ → (𝑋 ∈ AC 𝐴 ↔ 𝑋 ∈ V)) |
74 | 60, 73 | syl5ibr 236 |
. . . 4
⊢ (𝐴 = ∅ → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴)) |
75 | 67, 74 | pm2.61d2 172 |
. . 3
⊢ (𝑓:𝐴–1-1→𝐵 → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴)) |
76 | 75 | exlimiv 1858 |
. 2
⊢
(∃𝑓 𝑓:𝐴–1-1→𝐵 → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴)) |
77 | 1, 76 | syl 17 |
1
⊢ (𝐴 ≼ 𝐵 → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴)) |