Description: Lemma for frege118 . Proposition 117 of Frege1879 p. 78. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | frege116.x | ⊢ 𝑋 ∈ 𝑈 | |
Assertion | frege117 | ⊢ ( ( ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) → ( Fun ◡ ◡ 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege116.x | ⊢ 𝑋 ∈ 𝑈 | |
2 | 1 | frege116 | ⊢ ( Fun ◡ ◡ 𝑅 → ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) |
3 | frege9 | ⊢ ( ( Fun ◡ ◡ 𝑅 → ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) → ( ( ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) → ( Fun ◡ ◡ 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) ) ) | |
4 | 2 3 | ax-mp | ⊢ ( ( ∀ 𝑏 ( 𝑏 𝑅 𝑋 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑋 ) ) → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) → ( Fun ◡ ◡ 𝑅 → ( 𝑌 𝑅 𝑋 → ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 = 𝑋 ) ) ) ) |