Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
⊢ 𝑥 ∈ V |
2 |
1
|
elima3 |
⊢ ( 𝑥 ∈ ( { 〈 𝐴 , 𝐴 〉 } “ { 𝐵 } ) ↔ ∃ 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ 〈 𝑦 , 𝑥 〉 ∈ { 〈 𝐴 , 𝐴 〉 } ) ) |
3 |
|
velsn |
⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 ) |
4 |
2 3
|
imbi12i |
⊢ ( ( 𝑥 ∈ ( { 〈 𝐴 , 𝐴 〉 } “ { 𝐵 } ) → 𝑥 ∈ { 𝐵 } ) ↔ ( ∃ 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ 〈 𝑦 , 𝑥 〉 ∈ { 〈 𝐴 , 𝐴 〉 } ) → 𝑥 = 𝐵 ) ) |
5 |
4
|
albii |
⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( { 〈 𝐴 , 𝐴 〉 } “ { 𝐵 } ) → 𝑥 ∈ { 𝐵 } ) ↔ ∀ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ 〈 𝑦 , 𝑥 〉 ∈ { 〈 𝐴 , 𝐴 〉 } ) → 𝑥 = 𝐵 ) ) |
6 |
|
velsn |
⊢ ( 𝑦 ∈ { 𝐵 } ↔ 𝑦 = 𝐵 ) |
7 |
|
opex |
⊢ 〈 𝑦 , 𝑥 〉 ∈ V |
8 |
7
|
elsn |
⊢ ( 〈 𝑦 , 𝑥 〉 ∈ { 〈 𝐴 , 𝐴 〉 } ↔ 〈 𝑦 , 𝑥 〉 = 〈 𝐴 , 𝐴 〉 ) |
9 |
|
vex |
⊢ 𝑦 ∈ V |
10 |
9 1
|
opth |
⊢ ( 〈 𝑦 , 𝑥 〉 = 〈 𝐴 , 𝐴 〉 ↔ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) ) |
11 |
8 10
|
bitri |
⊢ ( 〈 𝑦 , 𝑥 〉 ∈ { 〈 𝐴 , 𝐴 〉 } ↔ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) ) |
12 |
6 11
|
anbi12i |
⊢ ( ( 𝑦 ∈ { 𝐵 } ∧ 〈 𝑦 , 𝑥 〉 ∈ { 〈 𝐴 , 𝐴 〉 } ) ↔ ( 𝑦 = 𝐵 ∧ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) ) ) |
13 |
|
3anass |
⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) ↔ ( 𝑦 = 𝐵 ∧ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) ) ) |
14 |
12 13
|
bitr4i |
⊢ ( ( 𝑦 ∈ { 𝐵 } ∧ 〈 𝑦 , 𝑥 〉 ∈ { 〈 𝐴 , 𝐴 〉 } ) ↔ ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) ) |
15 |
|
simp3 |
⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 ) |
16 |
|
simp2 |
⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → 𝑦 = 𝐴 ) |
17 |
|
simp1 |
⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → 𝑦 = 𝐵 ) |
18 |
15 16 17
|
3eqtr2d |
⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐵 ) |
19 |
14 18
|
sylbi |
⊢ ( ( 𝑦 ∈ { 𝐵 } ∧ 〈 𝑦 , 𝑥 〉 ∈ { 〈 𝐴 , 𝐴 〉 } ) → 𝑥 = 𝐵 ) |
20 |
19
|
exlimiv |
⊢ ( ∃ 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ 〈 𝑦 , 𝑥 〉 ∈ { 〈 𝐴 , 𝐴 〉 } ) → 𝑥 = 𝐵 ) |
21 |
5 20
|
mpgbir |
⊢ ∀ 𝑥 ( 𝑥 ∈ ( { 〈 𝐴 , 𝐴 〉 } “ { 𝐵 } ) → 𝑥 ∈ { 𝐵 } ) |
22 |
|
dfss2 |
⊢ ( ( { 〈 𝐴 , 𝐴 〉 } “ { 𝐵 } ) ⊆ { 𝐵 } ↔ ∀ 𝑥 ( 𝑥 ∈ ( { 〈 𝐴 , 𝐴 〉 } “ { 𝐵 } ) → 𝑥 ∈ { 𝐵 } ) ) |
23 |
21 22
|
mpbir |
⊢ ( { 〈 𝐴 , 𝐴 〉 } “ { 𝐵 } ) ⊆ { 𝐵 } |
24 |
|
df-he |
⊢ ( { 〈 𝐴 , 𝐴 〉 } hereditary { 𝐵 } ↔ ( { 〈 𝐴 , 𝐴 〉 } “ { 𝐵 } ) ⊆ { 𝐵 } ) |
25 |
23 24
|
mpbir |
⊢ { 〈 𝐴 , 𝐴 〉 } hereditary { 𝐵 } |