Step |
Hyp |
Ref |
Expression |
1 |
|
ac6.1 |
⊢ 𝐴 ∈ V |
2 |
|
ac6.2 |
⊢ 𝐵 ∈ V |
3 |
|
ac6.3 |
⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) |
4 |
|
ssrab2 |
⊢ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵 |
5 |
4
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵 |
6 |
|
iunss |
⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵 ) |
7 |
5 6
|
mpbir |
⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵 |
8 |
2 7
|
ssexi |
⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V |
9 |
|
numth3 |
⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ) |
10 |
8 9
|
ax-mp |
⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card |
11 |
3
|
ac6num |
⊢ ( ( 𝐴 ∈ V ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) |
12 |
1 10 11
|
mp3an12 |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) |