Theorem erdszelem1

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

	Ref	Expression
Hypothesis	erdszelem1.1	⊢ 𝑆 = { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) }
Assertion	erdszelem1	⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		erdszelem1.1	⊢ 𝑆 = { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) }
2		ovex	⊢ ( 1 ... 𝐴 ) ∈ V
3	2	elpw2	⊢ ( 𝑋 ∈ 𝒫 ( 1 ... 𝐴 ) ↔ 𝑋 ⊆ ( 1 ... 𝐴 ) )
4	3	anbi1i	⊢ ( ( 𝑋 ∈ 𝒫 ( 1 ... 𝐴 ) ∧ ( ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ) ↔ ( 𝑋 ⊆ ( 1 ... 𝐴 ) ∧ ( ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ) )
5		reseq2	⊢ ( 𝑦 = 𝑋 → ( 𝐹 ↾ 𝑦 ) = ( 𝐹 ↾ 𝑋 ) )
6		isoeq1	⊢ ( ( 𝐹 ↾ 𝑦 ) = ( 𝐹 ↾ 𝑋 ) → ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ↔ ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ) )
7	5 6	syl	⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ↔ ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ) )
8		isoeq4	⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ↔ ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑦 ) ) ) )
9		imaeq2	⊢ ( 𝑦 = 𝑋 → ( 𝐹 “ 𝑦 ) = ( 𝐹 “ 𝑋 ) )
10		isoeq5	⊢ ( ( 𝐹 “ 𝑦 ) = ( 𝐹 “ 𝑋 ) → ( ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑦 ) ) ↔ ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ) )
11	9 10	syl	⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑦 ) ) ↔ ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ) )
12	7 8 11	3bitrd	⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ↔ ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ) )
13		eleq2	⊢ ( 𝑦 = 𝑋 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑋 ) )
14	12 13	anbi12d	⊢ ( 𝑦 = 𝑋 → ( ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) ↔ ( ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ) )
15	14 1	elrab2	⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝒫 ( 1 ... 𝐴 ) ∧ ( ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ) )
16		3anass	⊢ ( ( 𝑋 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ↔ ( 𝑋 ⊆ ( 1 ... 𝐴 ) ∧ ( ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ) )
17	4 15 16	3bitr4i	⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑋 ) Isom < , 𝑂 ( 𝑋 , ( 𝐹 “ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) )