Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → 𝐹 : 𝑆 ⟶ 𝑇 ) |
2 |
|
simp2l |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → 𝑋 ∈ 𝑉 ) |
3 |
|
simp3 |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → 𝑌 ∈ 𝑇 ) |
4 |
|
f1osng |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑇 ) → { 〈 𝑋 , 𝑌 〉 } : { 𝑋 } –1-1-onto→ { 𝑌 } ) |
5 |
2 3 4
|
syl2anc |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → { 〈 𝑋 , 𝑌 〉 } : { 𝑋 } –1-1-onto→ { 𝑌 } ) |
6 |
|
f1of |
⊢ ( { 〈 𝑋 , 𝑌 〉 } : { 𝑋 } –1-1-onto→ { 𝑌 } → { 〈 𝑋 , 𝑌 〉 } : { 𝑋 } ⟶ { 𝑌 } ) |
7 |
5 6
|
syl |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → { 〈 𝑋 , 𝑌 〉 } : { 𝑋 } ⟶ { 𝑌 } ) |
8 |
|
simp2r |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ¬ 𝑋 ∈ 𝑆 ) |
9 |
|
disjsn |
⊢ ( ( 𝑆 ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ 𝑆 ) |
10 |
8 9
|
sylibr |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝑆 ∩ { 𝑋 } ) = ∅ ) |
11 |
|
fun |
⊢ ( ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ { 〈 𝑋 , 𝑌 〉 } : { 𝑋 } ⟶ { 𝑌 } ) ∧ ( 𝑆 ∩ { 𝑋 } ) = ∅ ) → ( 𝐹 ∪ { 〈 𝑋 , 𝑌 〉 } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ ( 𝑇 ∪ { 𝑌 } ) ) |
12 |
1 7 10 11
|
syl21anc |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { 〈 𝑋 , 𝑌 〉 } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ ( 𝑇 ∪ { 𝑌 } ) ) |
13 |
|
snssi |
⊢ ( 𝑌 ∈ 𝑇 → { 𝑌 } ⊆ 𝑇 ) |
14 |
13
|
3ad2ant3 |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → { 𝑌 } ⊆ 𝑇 ) |
15 |
|
ssequn2 |
⊢ ( { 𝑌 } ⊆ 𝑇 ↔ ( 𝑇 ∪ { 𝑌 } ) = 𝑇 ) |
16 |
14 15
|
sylib |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝑇 ∪ { 𝑌 } ) = 𝑇 ) |
17 |
16
|
feq3d |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( ( 𝐹 ∪ { 〈 𝑋 , 𝑌 〉 } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ ( 𝑇 ∪ { 𝑌 } ) ↔ ( 𝐹 ∪ { 〈 𝑋 , 𝑌 〉 } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ 𝑇 ) ) |
18 |
12 17
|
mpbid |
⊢ ( ( 𝐹 : 𝑆 ⟶ 𝑇 ∧ ( 𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑌 ∈ 𝑇 ) → ( 𝐹 ∪ { 〈 𝑋 , 𝑌 〉 } ) : ( 𝑆 ∪ { 𝑋 } ) ⟶ 𝑇 ) |