| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
| 2 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ 𝑋 ∈ dom
card) |
| 3 | | elmapi 8889 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴)
→ 𝑓:𝐴⟶(𝒫 𝑋 ∖ {∅})) |
| 4 | 3 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ 𝑓:𝐴⟶(𝒫 𝑋 ∖ {∅})) |
| 5 | 4 | frnd 6744 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ ran 𝑓 ⊆
(𝒫 𝑋 ∖
{∅})) |
| 6 | 5 | difss2d 4139 |
. . . . . . . . 9
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ ran 𝑓 ⊆
𝒫 𝑋) |
| 7 | | sspwuni 5100 |
. . . . . . . . 9
⊢ (ran
𝑓 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝑓 ⊆ 𝑋) |
| 8 | 6, 7 | sylib 218 |
. . . . . . . 8
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ ∪ ran 𝑓 ⊆ 𝑋) |
| 9 | | ssnum 10079 |
. . . . . . . 8
⊢ ((𝑋 ∈ dom card ∧ ∪ ran 𝑓 ⊆ 𝑋) → ∪ ran
𝑓 ∈ dom
card) |
| 10 | 2, 8, 9 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ ∪ ran 𝑓 ∈ dom card) |
| 11 | | ssdifin0 4486 |
. . . . . . . . 9
⊢ (ran
𝑓 ⊆ (𝒫 𝑋 ∖ {∅}) → (ran
𝑓 ∩ {∅}) =
∅) |
| 12 | 5, 11 | syl 17 |
. . . . . . . 8
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ (ran 𝑓 ∩
{∅}) = ∅) |
| 13 | | disjsn 4711 |
. . . . . . . 8
⊢ ((ran
𝑓 ∩ {∅}) =
∅ ↔ ¬ ∅ ∈ ran 𝑓) |
| 14 | 12, 13 | sylib 218 |
. . . . . . 7
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ ¬ ∅ ∈ ran 𝑓) |
| 15 | | ac5num 10076 |
. . . . . . 7
⊢ ((∪ ran 𝑓 ∈ dom card ∧ ¬ ∅ ∈
ran 𝑓) → ∃ℎ(ℎ:ran 𝑓⟶∪ ran
𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) |
| 16 | 10, 14, 15 | syl2anc 584 |
. . . . . 6
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ ∃ℎ(ℎ:ran 𝑓⟶∪ ran
𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) |
| 17 | | simpllr 776 |
. . . . . . 7
⊢ ((((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
∧ (ℎ:ran 𝑓⟶∪ ran 𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) → 𝐴 ∈ V) |
| 18 | 4 | ffnd 6737 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ 𝑓 Fn 𝐴) |
| 19 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑓‘𝑥) → (ℎ‘𝑦) = (ℎ‘(𝑓‘𝑥))) |
| 20 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑓‘𝑥) → 𝑦 = (𝑓‘𝑥)) |
| 21 | 19, 20 | eleq12d 2835 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑓‘𝑥) → ((ℎ‘𝑦) ∈ 𝑦 ↔ (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
| 22 | 21 | ralrn 7108 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝐴 → (∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦 ↔ ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
| 23 | 18, 22 | syl 17 |
. . . . . . . . 9
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ (∀𝑦 ∈
ran 𝑓(ℎ‘𝑦) ∈ 𝑦 ↔ ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))) |
| 24 | 23 | biimpa 476 |
. . . . . . . 8
⊢ ((((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
∧ ∀𝑦 ∈ ran
𝑓(ℎ‘𝑦) ∈ 𝑦) → ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)) |
| 25 | 24 | adantrl 716 |
. . . . . . 7
⊢ ((((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
∧ (ℎ:ran 𝑓⟶∪ ran 𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) → ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)) |
| 26 | | acnlem 10088 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 (ℎ‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) |
| 27 | 17, 25, 26 | syl2anc 584 |
. . . . . 6
⊢ ((((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
∧ (ℎ:ran 𝑓⟶∪ ran 𝑓 ∧ ∀𝑦 ∈ ran 𝑓(ℎ‘𝑦) ∈ 𝑦)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) |
| 28 | 16, 27 | exlimddv 1935 |
. . . . 5
⊢ (((𝑋 ∈ dom card ∧ 𝐴 ∈ V) ∧ 𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴))
→ ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) |
| 29 | 28 | ralrimiva 3146 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ 𝐴 ∈ V) → ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) |
| 30 | | isacn 10084 |
. . . 4
⊢ ((𝑋 ∈ dom card ∧ 𝐴 ∈ V) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅})
↑m 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥))) |
| 31 | 29, 30 | mpbird 257 |
. . 3
⊢ ((𝑋 ∈ dom card ∧ 𝐴 ∈ V) → 𝑋 ∈ AC 𝐴) |
| 32 | 31 | expcom 413 |
. 2
⊢ (𝐴 ∈ V → (𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴)) |
| 33 | 1, 32 | syl 17 |
1
⊢ (𝐴 ∈ 𝑉 → (𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴)) |