Step |
Hyp |
Ref |
Expression |
1 |
|
frege87.x |
⊢ 𝑋 ∈ 𝑈 |
2 |
|
frege87.y |
⊢ 𝑌 ∈ 𝑉 |
3 |
|
frege87.z |
⊢ 𝑍 ∈ 𝑊 |
4 |
|
frege87.r |
⊢ 𝑅 ∈ 𝑆 |
5 |
|
frege87.a |
⊢ 𝐴 ∈ 𝐵 |
6 |
1 2 3 4 5
|
frege87 |
⊢ ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → ( 𝑌 𝑅 𝑍 → 𝑍 ∈ 𝐴 ) ) ) ) |
7 |
|
frege15 |
⊢ ( ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → ( 𝑌 𝑅 𝑍 → 𝑍 ∈ 𝐴 ) ) ) ) → ( 𝑌 𝑅 𝑍 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → 𝑍 ∈ 𝐴 ) ) ) ) ) |
8 |
6 7
|
ax-mp |
⊢ ( 𝑌 𝑅 𝑍 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝐴 ) → ( 𝑅 hereditary 𝐴 → 𝑍 ∈ 𝐴 ) ) ) ) |