Theorem frege70

Description: Lemma for frege72 . Proposition 70 of Frege1879 p. 58. (Contributed by RP, 28-Mar-2020) (Revised by RP, 3-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	frege70.x	⊢ 𝑋 ∈ 𝑉
Assertion	frege70	⊢ ( 𝑅 hereditary 𝐴 → ( 𝑋 ∈ 𝐴 → ∀ 𝑦 ( 𝑋 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frege70.x	⊢ 𝑋 ∈ 𝑉
2		dffrege69	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ 𝑅 hereditary 𝐴 )
3	1	frege68c	⊢ ( ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ 𝑅 hereditary 𝐴 ) → ( 𝑅 hereditary 𝐴 → [ 𝑋 / 𝑥 ] ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
4		sbcel1v	⊢ ( [ 𝑋 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 )
5	4	biimpri	⊢ ( 𝑋 ∈ 𝐴 → [ 𝑋 / 𝑥 ] 𝑥 ∈ 𝐴 )
6		sbcim1	⊢ ( [ 𝑋 / 𝑥 ] ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) → ( [ 𝑋 / 𝑥 ] 𝑥 ∈ 𝐴 → [ 𝑋 / 𝑥 ] ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )
7		sbcal	⊢ ( [ 𝑋 / 𝑥 ] ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ↔ ∀ 𝑦 [ 𝑋 / 𝑥 ] ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) )
8		sbcim1	⊢ ( [ 𝑋 / 𝑥 ] ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) → ( [ 𝑋 / 𝑥 ] 𝑥 𝑅 𝑦 → [ 𝑋 / 𝑥 ] 𝑦 ∈ 𝐴 ) )
9		sbcbr1g	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝑥 𝑅 𝑦 ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝑥 𝑅 𝑦 ) )
10	1 9	ax-mp	⊢ ( [ 𝑋 / 𝑥 ] 𝑥 𝑅 𝑦 ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝑥 𝑅 𝑦 )
11		csbvarg	⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑥 ⦌ 𝑥 = 𝑋 )
12	1 11	ax-mp	⊢ ⦋ 𝑋 / 𝑥 ⦌ 𝑥 = 𝑋
13	12	breq1i	⊢ ( ⦋ 𝑋 / 𝑥 ⦌ 𝑥 𝑅 𝑦 ↔ 𝑋 𝑅 𝑦 )
14	10 13	bitri	⊢ ( [ 𝑋 / 𝑥 ] 𝑥 𝑅 𝑦 ↔ 𝑋 𝑅 𝑦 )
15		sbcg	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
16	1 15	ax-mp	⊢ ( [ 𝑋 / 𝑥 ] 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 )
17	8 14 16	3imtr3g	⊢ ( [ 𝑋 / 𝑥 ] ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) → ( 𝑋 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) )
18	17	alimi	⊢ ( ∀ 𝑦 [ 𝑋 / 𝑥 ] ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑋 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) )
19	7 18	sylbi	⊢ ( [ 𝑋 / 𝑥 ] ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑋 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) )
20	5 6 19	syl56	⊢ ( [ 𝑋 / 𝑥 ] ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) → ( 𝑋 ∈ 𝐴 → ∀ 𝑦 ( 𝑋 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )
21	3 20	syl6	⊢ ( ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ↔ 𝑅 hereditary 𝐴 ) → ( 𝑅 hereditary 𝐴 → ( 𝑋 ∈ 𝐴 → ∀ 𝑦 ( 𝑋 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) ) )
22	2 21	ax-mp	⊢ ( 𝑅 hereditary 𝐴 → ( 𝑋 ∈ 𝐴 → ∀ 𝑦 ( 𝑋 𝑅 𝑦 → 𝑦 ∈ 𝐴 ) ) )