Theorem htaOLD

Description: Obsolete version of hta as of 22-Jul-2026. (Contributed by NM, 11-Mar-2004) (Revised by Mario Carneiro, 25-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	htaOLD.1	⊢ 𝐴 = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
	htaOLD.2	⊢ 𝐵 = ( ℩ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 )
Assertion	htaOLD	⊢ ( 𝑅 We 𝐴 → ( 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		htaOLD.1	⊢ 𝐴 = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
2		htaOLD.2	⊢ 𝐵 = ( ℩ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 )
3		19.8a	⊢ ( 𝜑 → ∃ 𝑥 𝜑 )
4		scott0bsOLD	⊢ ( ∃ 𝑥 𝜑 ↔ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ≠ ∅ )
5	1	neeq1i	⊢ ( 𝐴 ≠ ∅ ↔ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ≠ ∅ )
6	4 5	bitr4i	⊢ ( ∃ 𝑥 𝜑 ↔ 𝐴 ≠ ∅ )
7	3 6	sylib	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
8		scottexsOLD	⊢ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ∈ V
9	1 8	eqeltri	⊢ 𝐴 ∈ V
10	9 2	htalem	⊢ ( ( 𝑅 We 𝐴 ∧ 𝐴 ≠ ∅ ) → 𝐵 ∈ 𝐴 )
11	10	ex	⊢ ( 𝑅 We 𝐴 → ( 𝐴 ≠ ∅ → 𝐵 ∈ 𝐴 ) )
12		simpl	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝜑 )
13	12	ss2abi	⊢ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ⊆ { 𝑥 ∣ 𝜑 }
14	1 13	eqsstri	⊢ 𝐴 ⊆ { 𝑥 ∣ 𝜑 }
15	14	sseli	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ { 𝑥 ∣ 𝜑 } )
16		df-sbc	⊢ ( [ 𝐵 / 𝑥 ] 𝜑 ↔ 𝐵 ∈ { 𝑥 ∣ 𝜑 } )
17	15 16	sylibr	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 / 𝑥 ] 𝜑 )
18	7 11 17	syl56	⊢ ( 𝑅 We 𝐴 → ( 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) )