Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | simpll 786 |
. . . . . . . 8
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → 𝑋 ∈ dom card) |
3 | | elmapi 7765 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴) → 𝑓:𝐴⟶(𝒫 𝑋 ∖ {∅})) |
4 | 3 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → 𝑓:𝐴⟶(𝒫 𝑋 ∖ {∅})) |
5 | | frn 5966 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴⟶(𝒫 𝑋 ∖ {∅}) → ran 𝑓 ⊆ (𝒫 𝑋 ∖
{∅})) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ran 𝑓 ⊆ (𝒫 𝑋 ∖ {∅})) |
7 | 6 | difss2d 3702 |
. . . . . . . . 9
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ran 𝑓 ⊆ 𝒫 𝑋) |
8 | | sspwuni 4547 |
. . . . . . . . 9
⊢ (ran
𝑓 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝑓 ⊆ 𝑋) |
9 | 7, 8 | sylib 207 |
. . . . . . . 8
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ∪ ran
𝑓 ⊆ 𝑋) |
10 | | ssnum 8745 |
. . . . . . . 8
⊢ ((𝑋 ∈ dom card ∧ ∪ ran 𝑓 ⊆ 𝑋) → ∪ ran
𝑓 ∈ dom
card) |
11 | 2, 9, 10 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ∪ ran
𝑓 ∈ dom
card) |
12 | | ssdifin0 4002 |
. . . . . . . . 9
⊢ (ran
𝑓 ⊆ (𝒫 𝑋 ∖ {∅}) → (ran
𝑓 ∩ {∅}) =
∅) |
13 | 6, 12 | syl 17 |
. . . . . . . 8
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → (ran 𝑓 ∩ {∅}) = ∅) |
14 | | disjsn 4192 |
. . . . . . . 8
⊢ ((ran
𝑓 ∩ {∅}) =
∅ ↔ ¬ ∅ ∈ ran 𝑓) |
15 | 13, 14 | sylib 207 |
. . . . . . 7
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ¬ ∅ ∈ ran 𝑓) |
16 | | ac5num 8742 |
. . . . . . 7
⊢ ((∪ ran 𝑓 ∈ dom card ∧ ¬ ∅ ∈
ran 𝑓) → ∃ℎ(ℎ:ran 𝑓⟶∪ ran
𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) |
17 | 11, 15, 16 | syl2anc 691 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ∃ℎ(ℎ:ran 𝑓⟶∪ ran
𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) |
18 | | simpllr 795 |
. . . . . . 7
⊢ ((((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ (ℎ:ran 𝑓⟶∪ ran
𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) → 𝐴 ∈ V) |
19 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴⟶(𝒫 𝑋 ∖ {∅}) → 𝑓 Fn 𝐴) |
20 | 4, 19 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → 𝑓 Fn 𝐴) |
21 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑓‘𝑥) → (ℎ‘𝑦) = (ℎ‘(𝑓‘𝑥))) |
22 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑓‘𝑥) → 𝑦 = (𝑓‘𝑥)) |
23 | 21, 22 | eleq12d 2682 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑓‘𝑥) → ((ℎ‘𝑦) ∈ 𝑦 ↔ (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
24 | 23 | ralrn 6270 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝐴 → (∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦 ↔ ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
25 | 20, 24 | syl 17 |
. . . . . . . . 9
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → (∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦 ↔ ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
26 | 25 | biimpa 500 |
. . . . . . . 8
⊢ ((((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦) → ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)) |
27 | 26 | adantrl 748 |
. . . . . . 7
⊢ ((((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ (ℎ:ran 𝑓⟶∪ ran
𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) → ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)) |
28 | | acnlem 8754 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) |
29 | 18, 27, 28 | syl2anc 691 |
. . . . . 6
⊢ ((((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) ∧ (ℎ:ran 𝑓⟶∪ ran
𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) |
30 | 17, 29 | exlimddv 1850 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) |
31 | 30 | ralrimiva 2949 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ 𝐴 ∈ V) → ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) |
32 | | isacn 8750 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ 𝐴 ∈ V) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑𝑚 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥))) |
33 | 31, 32 | mpbird 246 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ 𝐴 ∈ V) → 𝑋 ∈ AC 𝐴) |
34 | 33 | expcom 450 |
. 2
⊢ (𝐴 ∈ V → (𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴)) |
35 | 1, 34 | syl 17 |
1
⊢ (𝐴 ∈ 𝑉 → (𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴)) |