Step |
Hyp |
Ref |
Expression |
1 |
|
frege77d.r |
⊢ ( 𝜑 → 𝑅 ∈ V ) |
2 |
|
frege77d.a |
⊢ ( 𝜑 → 𝐴 ∈ V ) |
3 |
|
frege77d.b |
⊢ ( 𝜑 → 𝐵 ∈ V ) |
4 |
|
frege77d.ab |
⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ) |
5 |
|
frege77d.he |
⊢ ( 𝜑 → ( 𝑅 “ 𝑈 ) ⊆ 𝑈 ) |
6 |
|
frege77d.ss |
⊢ ( 𝜑 → ( 𝑅 “ { 𝐴 } ) ⊆ 𝑈 ) |
7 |
|
imaundi |
⊢ ( 𝑅 “ ( { 𝐴 } ∪ 𝑈 ) ) = ( ( 𝑅 “ { 𝐴 } ) ∪ ( 𝑅 “ 𝑈 ) ) |
8 |
6 5
|
unssd |
⊢ ( 𝜑 → ( ( 𝑅 “ { 𝐴 } ) ∪ ( 𝑅 “ 𝑈 ) ) ⊆ 𝑈 ) |
9 |
7 8
|
eqsstrid |
⊢ ( 𝜑 → ( 𝑅 “ ( { 𝐴 } ∪ 𝑈 ) ) ⊆ 𝑈 ) |
10 |
|
trclimalb2 |
⊢ ( ( 𝑅 ∈ V ∧ ( 𝑅 “ ( { 𝐴 } ∪ 𝑈 ) ) ⊆ 𝑈 ) → ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) ⊆ 𝑈 ) |
11 |
1 9 10
|
syl2anc |
⊢ ( 𝜑 → ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) ⊆ 𝑈 ) |
12 |
|
df-br |
⊢ ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ↔ 〈 𝐴 , 𝐵 〉 ∈ ( t+ ‘ 𝑅 ) ) |
13 |
4 12
|
sylib |
⊢ ( 𝜑 → 〈 𝐴 , 𝐵 〉 ∈ ( t+ ‘ 𝑅 ) ) |
14 |
|
elimasng |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐵 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) ↔ 〈 𝐴 , 𝐵 〉 ∈ ( t+ ‘ 𝑅 ) ) ) |
15 |
2 3 14
|
syl2anc |
⊢ ( 𝜑 → ( 𝐵 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) ↔ 〈 𝐴 , 𝐵 〉 ∈ ( t+ ‘ 𝑅 ) ) ) |
16 |
13 15
|
mpbird |
⊢ ( 𝜑 → 𝐵 ∈ ( ( t+ ‘ 𝑅 ) “ { 𝐴 } ) ) |
17 |
11 16
|
sseldd |
⊢ ( 𝜑 → 𝐵 ∈ 𝑈 ) |