Description: One direction of dffrege76 . Proposition 89 of Frege1879 p. 68. (Contributed by RP, 1-Jul-2020) (Revised by RP, 2-Jul-2020) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frege89.x | ⊢ 𝑋 ∈ 𝑈 | |
frege89.y | ⊢ 𝑌 ∈ 𝑉 | ||
frege89.r | ⊢ 𝑅 ∈ 𝑊 | ||
Assertion | frege89 | ⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege89.x | ⊢ 𝑋 ∈ 𝑈 | |
2 | frege89.y | ⊢ 𝑌 ∈ 𝑉 | |
3 | frege89.r | ⊢ 𝑅 ∈ 𝑊 | |
4 | 1 2 3 | dffrege76 | ⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) |
5 | frege52aid | ⊢ ( ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) ↔ 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) → ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) ) | |
6 | 4 5 | ax-mp | ⊢ ( ∀ 𝑓 ( 𝑅 hereditary 𝑓 → ( ∀ 𝑤 ( 𝑋 𝑅 𝑤 → 𝑤 ∈ 𝑓 ) → 𝑌 ∈ 𝑓 ) ) → 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ) |