Metamath Proof Explorer

Theorem erdszelem4

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

Ref Expression
Hypotheses erdsze.n ⊒ ( πœ‘ β†’ 𝑁 ∈ β„• )
erdsze.f ⊒ ( πœ‘ β†’ 𝐹 : ( 1 ... 𝑁 ) –1-1β†’ ℝ )
erdszelem.k ⊒ 𝐾 = ( π‘₯ ∈ ( 1 ... 𝑁 ) ↦ sup ( ( β™― β€œ { 𝑦 ∈ 𝒫 ( 1 ... π‘₯ ) ∣ ( ( 𝐹 β†Ύ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 β€œ 𝑦 ) ) ∧ π‘₯ ∈ 𝑦 ) } ) , ℝ , < ) )
erdszelem.o ⊒ 𝑂 Or ℝ
Assertion erdszelem4 ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ { 𝐴 } ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 β†Ύ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 β€œ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } )

Proof

Step Hyp Ref Expression
1 erdsze.n ⊒ ( πœ‘ β†’ 𝑁 ∈ β„• )
2 erdsze.f ⊒ ( πœ‘ β†’ 𝐹 : ( 1 ... 𝑁 ) –1-1β†’ ℝ )
3 erdszelem.k ⊒ 𝐾 = ( π‘₯ ∈ ( 1 ... 𝑁 ) ↦ sup ( ( β™― β€œ { 𝑦 ∈ 𝒫 ( 1 ... π‘₯ ) ∣ ( ( 𝐹 β†Ύ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 β€œ 𝑦 ) ) ∧ π‘₯ ∈ 𝑦 ) } ) , ℝ , < ) )
4 erdszelem.o ⊒ 𝑂 Or ℝ
5 elfznn ⊒ ( 𝐴 ∈ ( 1 ... 𝑁 ) β†’ 𝐴 ∈ β„• )
6 5 adantl ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ 𝐴 ∈ β„• )
7 elfz1end ⊒ ( 𝐴 ∈ β„• ↔ 𝐴 ∈ ( 1 ... 𝐴 ) )
8 6 7 sylib ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ 𝐴 ∈ ( 1 ... 𝐴 ) )
9 8 snssd ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ { 𝐴 } βŠ† ( 1 ... 𝐴 ) )
10 elsni ⊒ ( π‘₯ ∈ { 𝐴 } β†’ π‘₯ = 𝐴 )
11 elsni ⊒ ( 𝑦 ∈ { 𝐴 } β†’ 𝑦 = 𝐴 )
12 10 11 breqan12d ⊒ ( ( π‘₯ ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) β†’ ( π‘₯ < 𝑦 ↔ 𝐴 < 𝐴 ) )
13 12 adantl ⊒ ( ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( π‘₯ ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) β†’ ( π‘₯ < 𝑦 ↔ 𝐴 < 𝐴 ) )
14 fzssuz ⊒ ( 1 ... 𝑁 ) βŠ† ( β„€β‰₯ β€˜ 1 )
15 uzssz ⊒ ( β„€β‰₯ β€˜ 1 ) βŠ† β„€
16 zssre ⊒ β„€ βŠ† ℝ
17 15 16 sstri ⊒ ( β„€β‰₯ β€˜ 1 ) βŠ† ℝ
18 14 17 sstri ⊒ ( 1 ... 𝑁 ) βŠ† ℝ
19 simpr ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ 𝐴 ∈ ( 1 ... 𝑁 ) )
20 19 adantr ⊒ ( ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( π‘₯ ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) β†’ 𝐴 ∈ ( 1 ... 𝑁 ) )
21 18 20 sselid ⊒ ( ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( π‘₯ ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) β†’ 𝐴 ∈ ℝ )
22 21 ltnrd ⊒ ( ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( π‘₯ ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) β†’ Β¬ 𝐴 < 𝐴 )
23 22 pm2.21d ⊒ ( ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( π‘₯ ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) β†’ ( 𝐴 < 𝐴 β†’ ( 𝐹 β€˜ π‘₯ ) 𝑂 ( 𝐹 β€˜ 𝑦 ) ) )
24 13 23 sylbid ⊒ ( ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) ∧ ( π‘₯ ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ) β†’ ( π‘₯ < 𝑦 β†’ ( 𝐹 β€˜ π‘₯ ) 𝑂 ( 𝐹 β€˜ 𝑦 ) ) )
25 24 ralrimivva ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ βˆ€ π‘₯ ∈ { 𝐴 } βˆ€ 𝑦 ∈ { 𝐴 } ( π‘₯ < 𝑦 β†’ ( 𝐹 β€˜ π‘₯ ) 𝑂 ( 𝐹 β€˜ 𝑦 ) ) )
26 f1f ⊒ ( 𝐹 : ( 1 ... 𝑁 ) –1-1β†’ ℝ β†’ 𝐹 : ( 1 ... 𝑁 ) ⟢ ℝ )
27 2 26 syl ⊒ ( πœ‘ β†’ 𝐹 : ( 1 ... 𝑁 ) ⟢ ℝ )
28 27 adantr ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ 𝐹 : ( 1 ... 𝑁 ) ⟢ ℝ )
29 19 snssd ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ { 𝐴 } βŠ† ( 1 ... 𝑁 ) )
30 ltso ⊒ < Or ℝ
31 soss ⊒ ( ( 1 ... 𝑁 ) βŠ† ℝ β†’ ( < Or ℝ β†’ < Or ( 1 ... 𝑁 ) ) )
32 18 30 31 mp2 ⊒ < Or ( 1 ... 𝑁 )
33 soisores ⊒ ( ( ( < Or ( 1 ... 𝑁 ) ∧ 𝑂 Or ℝ ) ∧ ( 𝐹 : ( 1 ... 𝑁 ) ⟢ ℝ ∧ { 𝐴 } βŠ† ( 1 ... 𝑁 ) ) ) β†’ ( ( 𝐹 β†Ύ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 β€œ { 𝐴 } ) ) ↔ βˆ€ π‘₯ ∈ { 𝐴 } βˆ€ 𝑦 ∈ { 𝐴 } ( π‘₯ < 𝑦 β†’ ( 𝐹 β€˜ π‘₯ ) 𝑂 ( 𝐹 β€˜ 𝑦 ) ) ) )
34 32 4 33 mpanl12 ⊒ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟢ ℝ ∧ { 𝐴 } βŠ† ( 1 ... 𝑁 ) ) β†’ ( ( 𝐹 β†Ύ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 β€œ { 𝐴 } ) ) ↔ βˆ€ π‘₯ ∈ { 𝐴 } βˆ€ 𝑦 ∈ { 𝐴 } ( π‘₯ < 𝑦 β†’ ( 𝐹 β€˜ π‘₯ ) 𝑂 ( 𝐹 β€˜ 𝑦 ) ) ) )
35 28 29 34 syl2anc ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ ( ( 𝐹 β†Ύ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 β€œ { 𝐴 } ) ) ↔ βˆ€ π‘₯ ∈ { 𝐴 } βˆ€ 𝑦 ∈ { 𝐴 } ( π‘₯ < 𝑦 β†’ ( 𝐹 β€˜ π‘₯ ) 𝑂 ( 𝐹 β€˜ 𝑦 ) ) ) )
36 25 35 mpbird ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ ( 𝐹 β†Ύ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 β€œ { 𝐴 } ) ) )
37 snidg ⊒ ( 𝐴 ∈ ( 1 ... 𝑁 ) β†’ 𝐴 ∈ { 𝐴 } )
38 37 adantl ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ 𝐴 ∈ { 𝐴 } )
39 eqid ⊒ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 β†Ύ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 β€œ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 β†Ύ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 β€œ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) }
40 39 erdszelem1 ⊒ ( { 𝐴 } ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 β†Ύ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 β€œ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ↔ ( { 𝐴 } βŠ† ( 1 ... 𝐴 ) ∧ ( 𝐹 β†Ύ { 𝐴 } ) Isom < , 𝑂 ( { 𝐴 } , ( 𝐹 β€œ { 𝐴 } ) ) ∧ 𝐴 ∈ { 𝐴 } ) )
41 9 36 38 40 syl3anbrc ⊒ ( ( πœ‘ ∧ 𝐴 ∈ ( 1 ... 𝑁 ) ) β†’ { 𝐴 } ∈ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 β†Ύ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 β€œ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } )