Metamath Proof Explorer

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 < , 𝑂 ( 𝑋 , ( 𝐹 β€œ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) )