Step |
Hyp |
Ref |
Expression |
1 |
|
frege94.x |
⊢ 𝑋 ∈ 𝑈 |
2 |
|
frege94.z |
⊢ 𝑍 ∈ 𝑉 |
3 |
|
frege94.r |
⊢ 𝑅 ∈ 𝑊 |
4 |
1 2 3
|
frege93 |
⊢ ( ∀ 𝑓 ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → ( 𝑅 hereditary 𝑓 → 𝑍 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ) |
5 |
|
frege7 |
⊢ ( ( ∀ 𝑓 ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → ( 𝑅 hereditary 𝑓 → 𝑍 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ) → ( ( 𝑌 𝑅 𝑍 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ∀ 𝑓 ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → ( 𝑅 hereditary 𝑓 → 𝑍 ∈ 𝑓 ) ) ) ) → ( 𝑌 𝑅 𝑍 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ) ) ) ) |
6 |
4 5
|
ax-mp |
⊢ ( ( 𝑌 𝑅 𝑍 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → ∀ 𝑓 ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → ( 𝑅 hereditary 𝑓 → 𝑍 ∈ 𝑓 ) ) ) ) → ( 𝑌 𝑅 𝑍 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 → 𝑋 ( t+ ‘ 𝑅 ) 𝑍 ) ) ) |