Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Additional statements on relations and subclasses
Adapted from Frege
frege81d
Metamath Proof Explorer
Description: If the image of U is a subset U , A is an element of U
and B follows A in the transitive closure of R , then B
is an element of U . Similar to Proposition 81 of Frege1879
p. 63. Compare with frege81 . (Contributed by RP , 15-Jul-2020)
Ref
Expression
Hypotheses
frege81d.r
⊢ φ → R ∈ V
frege81d.a
⊢ φ → A ∈ U
frege81d.b
⊢ φ → B ∈ V
frege81d.ab
⊢ φ → A t+ ⁡ R B
frege81d.he
⊢ φ → R U ⊆ U
Assertion
frege81d
⊢ φ → B ∈ U
Proof
Step
Hyp
Ref
Expression
1
frege81d.r
⊢ φ → R ∈ V
2
frege81d.a
⊢ φ → A ∈ U
3
frege81d.b
⊢ φ → B ∈ V
4
frege81d.ab
⊢ φ → A t+ ⁡ R B
5
frege81d.he
⊢ φ → R U ⊆ U
6
2
elexd
⊢ φ → A ∈ V
7
2
snssd
⊢ φ → A ⊆ U
8
imass2
⊢ A ⊆ U → R A ⊆ R U
9
7 8
syl
⊢ φ → R A ⊆ R U
10
9 5
sstrd
⊢ φ → R A ⊆ U
11
1 6 3 4 5 10
frege77d
⊢ φ → B ∈ U