Metamath Proof Explorer

Theorem frege110

Description: Proposition 110 of Frege1879 p. 75. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege110.x ⊢ X ∈ A
frege110.y ⊢ Y ∈ B
frege110.m ⊢ M ∈ C
frege110.r ⊢ R ∈ D
Assertion frege110 ⊢ ∀ a Y R a → X t+ ⁡ R ∪ I a → Y t+ ⁡ R M → X t+ ⁡ R ∪ I M

Proof

Step Hyp Ref Expression
1 frege110.x ⊢ X ∈ A
2 frege110.y ⊢ Y ∈ B
3 frege110.m ⊢ M ∈ C
4 frege110.r ⊢ R ∈ D
5 1 4 frege109 ⊢ R hereditary t+ ⁡ R ∪ I X
6 imaundir ⊢ t+ ⁡ R ∪ I X = t+ ⁡ R X ∪ I X
7 fvex ⊢ t+ ⁡ R ∈ V
8 imaexg ⊢ t+ ⁡ R ∈ V → t+ ⁡ R X ∈ V
9 7 8 ax-mp ⊢ t+ ⁡ R X ∈ V
10 imai ⊢ I X = X
11 snex ⊢ X ∈ V
12 10 11 eqeltri ⊢ I X ∈ V
13 9 12 unex ⊢ t+ ⁡ R X ∪ I X ∈ V
14 6 13 eqeltri ⊢ t+ ⁡ R ∪ I X ∈ V
15 2 3 4 14 frege78 ⊢ R hereditary t+ ⁡ R ∪ I X → ∀ a Y R a → a ∈ t+ ⁡ R ∪ I X → Y t+ ⁡ R M → M ∈ t+ ⁡ R ∪ I X
16 1 elexi ⊢ X ∈ V
17 vex ⊢ a ∈ V
18 16 17 elimasn ⊢ a ∈ t+ ⁡ R ∪ I X ↔ X a ∈ t+ ⁡ R ∪ I
19 df-br ⊢ X t+ ⁡ R ∪ I a ↔ X a ∈ t+ ⁡ R ∪ I
20 18 19 bitr4i ⊢ a ∈ t+ ⁡ R ∪ I X ↔ X t+ ⁡ R ∪ I a
21 20 imbi2i ⊢ Y R a → a ∈ t+ ⁡ R ∪ I X ↔ Y R a → X t+ ⁡ R ∪ I a
22 21 albii ⊢ ∀ a Y R a → a ∈ t+ ⁡ R ∪ I X ↔ ∀ a Y R a → X t+ ⁡ R ∪ I a
23 3 elexi ⊢ M ∈ V
24 16 23 elimasn ⊢ M ∈ t+ ⁡ R ∪ I X ↔ X M ∈ t+ ⁡ R ∪ I
25 df-br ⊢ X t+ ⁡ R ∪ I M ↔ X M ∈ t+ ⁡ R ∪ I
26 24 25 bitr4i ⊢ M ∈ t+ ⁡ R ∪ I X ↔ X t+ ⁡ R ∪ I M
27 26 imbi2i ⊢ Y t+ ⁡ R M → M ∈ t+ ⁡ R ∪ I X ↔ Y t+ ⁡ R M → X t+ ⁡ R ∪ I M
28 15 22 27 3imtr3g ⊢ R hereditary t+ ⁡ R ∪ I X → ∀ a Y R a → X t+ ⁡ R ∪ I a → Y t+ ⁡ R M → X t+ ⁡ R ∪ I M
29 5 28 ax-mp ⊢ ∀ a Y R a → X t+ ⁡ R ∪ I a → Y t+ ⁡ R M → X t+ ⁡ R ∪ I M