Metamath Proof Explorer

Theorem frege130

Description: Lemma for frege131 . Proposition 130 of Frege1879 p. 84. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege130.m ⊢ M ∈ U
frege130.r ⊢ R ∈ V
Assertion frege130 ⊢ ∀ b ¬ b t+ ⁡ R M → M t+ ⁡ R ∪ I b → ∀ a b R a → ¬ a t+ ⁡ R M → M t+ ⁡ R ∪ I a → R hereditary t+ ⁡ R -1 M ∪ t+ ⁡ R ∪ I M → Fun ⁡ R -1 -1 → R hereditary t+ ⁡ R -1 M ∪ t+ ⁡ R ∪ I M

Proof

Step Hyp Ref Expression
1 frege130.m ⊢ M ∈ U
2 frege130.r ⊢ R ∈ V
3 vex ⊢ a ∈ V
4 vex ⊢ b ∈ V
5 3 4 1 2 frege129 ⊢ Fun ⁡ R -1 -1 → ¬ b t+ ⁡ R M → M t+ ⁡ R ∪ I b → b R a → ¬ a t+ ⁡ R M → M t+ ⁡ R ∪ I a
6 5 alrimdv ⊢ Fun ⁡ R -1 -1 → ¬ b t+ ⁡ R M → M t+ ⁡ R ∪ I b → ∀ a b R a → ¬ a t+ ⁡ R M → M t+ ⁡ R ∪ I a
7 6 alrimiv ⊢ Fun ⁡ R -1 -1 → ∀ b ¬ b t+ ⁡ R M → M t+ ⁡ R ∪ I b → ∀ a b R a → ¬ a t+ ⁡ R M → M t+ ⁡ R ∪ I a
8 frege9 ⊢ Fun ⁡ R -1 -1 → ∀ b ¬ b t+ ⁡ R M → M t+ ⁡ R ∪ I b → ∀ a b R a → ¬ a t+ ⁡ R M → M t+ ⁡ R ∪ I a → ∀ b ¬ b t+ ⁡ R M → M t+ ⁡ R ∪ I b → ∀ a b R a → ¬ a t+ ⁡ R M → M t+ ⁡ R ∪ I a → R hereditary t+ ⁡ R -1 M ∪ t+ ⁡ R ∪ I M → Fun ⁡ R -1 -1 → R hereditary t+ ⁡ R -1 M ∪ t+ ⁡ R ∪ I M
9 7 8 ax-mp ⊢ ∀ b ¬ b t+ ⁡ R M → M t+ ⁡ R ∪ I b → ∀ a b R a → ¬ a t+ ⁡ R M → M t+ ⁡ R ∪ I a → R hereditary t+ ⁡ R -1 M ∪ t+ ⁡ R ∪ I M → Fun ⁡ R -1 -1 → R hereditary t+ ⁡ R -1 M ∪ t+ ⁡ R ∪ I M