Step |
Hyp |
Ref |
Expression |
1 |
|
f1oabexg.1 |
⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) } |
2 |
|
elex |
⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V ) |
3 |
|
elex |
⊢ ( 𝐵 ∈ 𝐷 → 𝐵 ∈ V ) |
4 |
|
f1of |
⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 ) |
5 |
4
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) ) → 𝑓 : 𝐴 ⟶ 𝐵 ) |
6 |
|
simpl |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐴 ∈ V ) |
7 |
|
simpr |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐵 ∈ V ) |
8 |
5 6 7
|
fabexd |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) } ∈ V ) |
9 |
1 8
|
eqeltrid |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐹 ∈ V ) |
10 |
2 3 9
|
syl2an |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V ) |