Metamath Proof Explorer

Theorem frege93

Description: Necessary condition for two elements to be related by the transitive closure. Proposition 93 of Frege1879 p. 70. (Contributed by RP, 2-Jul-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege91.x ⊢ X ∈ U
frege91.y ⊢ Y ∈ V
frege91.r ⊢ R ∈ W
Assertion frege93 ⊢ ∀ f ∀ z X R z → z ∈ f → R hereditary f → Y ∈ f → X t+ ⁡ R Y

Proof

Step Hyp Ref Expression
1 frege91.x ⊢ X ∈ U
2 frege91.y ⊢ Y ∈ V
3 frege91.r ⊢ R ∈ W
4 vex ⊢ f ∈ V
5 4 frege60c ⊢ ∀ f ∀ z X R z → z ∈ f → R hereditary f → Y ∈ f → [˙f / f]˙ R hereditary f → [˙f / f]˙ ∀ z X R z → z ∈ f → [˙f / f]˙ Y ∈ f
6 sbcid ⊢ [˙f / f]˙ R hereditary f ↔ R hereditary f
7 sbcid ⊢ [˙f / f]˙ ∀ z X R z → z ∈ f ↔ ∀ z X R z → z ∈ f
8 sbcid ⊢ [˙f / f]˙ Y ∈ f ↔ Y ∈ f
9 7 8 imbi12i ⊢ [˙f / f]˙ ∀ z X R z → z ∈ f → [˙f / f]˙ Y ∈ f ↔ ∀ z X R z → z ∈ f → Y ∈ f
10 5 6 9 3imtr3g ⊢ ∀ f ∀ z X R z → z ∈ f → R hereditary f → Y ∈ f → R hereditary f → ∀ z X R z → z ∈ f → Y ∈ f
11 10 axc4i ⊢ ∀ f ∀ z X R z → z ∈ f → R hereditary f → Y ∈ f → ∀ f R hereditary f → ∀ z X R z → z ∈ f → Y ∈ f
12 1 2 3 frege90 ⊢ ∀ f ∀ z X R z → z ∈ f → R hereditary f → Y ∈ f → ∀ f R hereditary f → ∀ z X R z → z ∈ f → Y ∈ f → ∀ f ∀ z X R z → z ∈ f → R hereditary f → Y ∈ f → X t+ ⁡ R Y
13 11 12 ax-mp ⊢ ∀ f ∀ z X R z → z ∈ f → R hereditary f → Y ∈ f → X t+ ⁡ R Y