Step |
Hyp |
Ref |
Expression |
1 |
|
simp3 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 ) |
2 |
|
ustdiag |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ( I ↾ 𝑋 ) ⊆ 𝑉 ) |
3 |
2
|
3adant3 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋 ) → ( I ↾ 𝑋 ) ⊆ 𝑉 ) |
4 |
|
opelidres |
⊢ ( 𝐴 ∈ 𝑋 → ( 〈 𝐴 , 𝐴 〉 ∈ ( I ↾ 𝑋 ) ↔ 𝐴 ∈ 𝑋 ) ) |
5 |
4
|
ibir |
⊢ ( 𝐴 ∈ 𝑋 → 〈 𝐴 , 𝐴 〉 ∈ ( I ↾ 𝑋 ) ) |
6 |
5
|
3ad2ant3 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋 ) → 〈 𝐴 , 𝐴 〉 ∈ ( I ↾ 𝑋 ) ) |
7 |
3 6
|
sseldd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋 ) → 〈 𝐴 , 𝐴 〉 ∈ 𝑉 ) |
8 |
|
elimasng |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) ↔ 〈 𝐴 , 𝐴 〉 ∈ 𝑉 ) ) |
9 |
8
|
anidms |
⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) ↔ 〈 𝐴 , 𝐴 〉 ∈ 𝑉 ) ) |
10 |
9
|
biimpar |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 〈 𝐴 , 𝐴 〉 ∈ 𝑉 ) → 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) ) |
11 |
1 7 10
|
syl2anc |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) ) |