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 ⊢∀aYRa→Xt+⁡R∪Ia→Yt+⁡RM→Xt+⁡R∪IM

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 ⊢Rhereditaryt+⁡R∪IX
6 imaundir ⊢t+⁡R∪IX=t+⁡RX∪IX
7 fvex ⊢t+⁡R∈V
8 imaexg ⊢t+⁡R∈V→t+⁡RX∈V
9 7 8 ax-mp ⊢t+⁡RX∈V
10 imai ⊢IX=X
11 snex ⊢X∈V
12 10 11 eqeltri ⊢IX∈V
13 9 12 unex ⊢t+⁡RX∪IX∈V
14 6 13 eqeltri ⊢t+⁡R∪IX∈V
15 2 3 4 14 frege78 ⊢Rhereditaryt+⁡R∪IX→∀aYRa→a∈t+⁡R∪IX→Yt+⁡RM→M∈t+⁡R∪IX
16 1 elexi ⊢X∈V
17 vex ⊢a∈V
18 16 17 elimasn ⊢a∈t+⁡R∪IX↔Xa∈t+⁡R∪I
19 df-br ⊢Xt+⁡R∪Ia↔Xa∈t+⁡R∪I
20 18 19 bitr4i ⊢a∈t+⁡R∪IX↔Xt+⁡R∪Ia
21 20 imbi2i ⊢YRa→a∈t+⁡R∪IX↔YRa→Xt+⁡R∪Ia
22 21 albii ⊢∀aYRa→a∈t+⁡R∪IX↔∀aYRa→Xt+⁡R∪Ia
23 3 elexi ⊢M∈V
24 16 23 elimasn ⊢M∈t+⁡R∪IX↔XM∈t+⁡R∪I
25 df-br ⊢Xt+⁡R∪IM↔XM∈t+⁡R∪I
26 24 25 bitr4i ⊢M∈t+⁡R∪IX↔Xt+⁡R∪IM
27 26 imbi2i ⊢Yt+⁡RM→M∈t+⁡R∪IX↔Yt+⁡RM→Xt+⁡R∪IM
28 15 22 27 3imtr3g ⊢Rhereditaryt+⁡R∪IX→∀aYRa→Xt+⁡R∪Ia→Yt+⁡RM→Xt+⁡R∪IM
29 5 28 ax-mp ⊢∀aYRa→Xt+⁡R∪Ia→Yt+⁡RM→Xt+⁡R∪IM