Theorem frege110

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

	Ref	Expression
Hypotheses	frege110.x	⊢ 𝑋 ∈ 𝐴
	frege110.y	⊢ 𝑌 ∈ 𝐵
	frege110.m	⊢ 𝑀 ∈ 𝐶
	frege110.r	⊢ 𝑅 ∈ 𝐷
Assertion	frege110	⊢ ( ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		frege110.x	⊢ 𝑋 ∈ 𝐴
2		frege110.y	⊢ 𝑌 ∈ 𝐵
3		frege110.m	⊢ 𝑀 ∈ 𝐶
4		frege110.r	⊢ 𝑅 ∈ 𝐷
5	1 4	frege109	⊢ 𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } )
6		imaundir	⊢ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) = ( ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ∪ ( I “ { 𝑋 } ) )
7		fvex	⊢ ( t+ ‘ 𝑅 ) ∈ V
8		imaexg	⊢ ( ( t+ ‘ 𝑅 ) ∈ V → ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ∈ V )
9	7 8	ax-mp	⊢ ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ∈ V
10		imai	⊢ ( I “ { 𝑋 } ) = { 𝑋 }
11		snex	⊢ { 𝑋 } ∈ V
12	10 11	eqeltri	⊢ ( I “ { 𝑋 } ) ∈ V
13	9 12	unex	⊢ ( ( ( t+ ‘ 𝑅 ) “ { 𝑋 } ) ∪ ( I “ { 𝑋 } ) ) ∈ V
14	6 13	eqeltri	⊢ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ∈ V
15	2 3 4 14	frege78	⊢ ( 𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) → ( ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ) → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ) ) )
16	1	elexi	⊢ 𝑋 ∈ V
17		vex	⊢ 𝑎 ∈ V
18	16 17	elimasn	⊢ ( 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑎 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
19		df-br	⊢ ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ↔ ⟨ 𝑋 , 𝑎 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
20	18 19	bitr4i	⊢ ( 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ↔ 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 )
21	20	imbi2i	⊢ ( ( 𝑌 𝑅 𝑎 → 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ) ↔ ( 𝑌 𝑅 𝑎 → 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) )
22	21	albii	⊢ ( ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑎 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ) ↔ ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) )
23	3	elexi	⊢ 𝑀 ∈ V
24	16 23	elimasn	⊢ ( 𝑀 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
25		df-br	⊢ ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ↔ ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ( t+ ‘ 𝑅 ) ∪ I ) )
26	24 25	bitr4i	⊢ ( 𝑀 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ↔ 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 )
27	26	imbi2i	⊢ ( ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑀 ∈ ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) ) ↔ ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ) )
28	15 22 27	3imtr3g	⊢ ( 𝑅 hereditary ( ( ( t+ ‘ 𝑅 ) ∪ I ) “ { 𝑋 } ) → ( ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ) ) )
29	5 28	ax-mp	⊢ ( ∀ 𝑎 ( 𝑌 𝑅 𝑎 → 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀 → 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ) )