Metamath Proof Explorer


Theorem fin23lem23

Description: Lemma for fin23lem22 . (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion fin23lem23 ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∃! 𝑗𝑆 ( 𝑗𝑆 ) ≈ 𝑖 )

Proof

Step Hyp Ref Expression
1 fin23lem26 ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∃ 𝑗𝑆 ( 𝑗𝑆 ) ≈ 𝑖 )
2 ensym ( ( 𝑎𝑆 ) ≈ 𝑖𝑖 ≈ ( 𝑎𝑆 ) )
3 entr ( ( ( 𝑗𝑆 ) ≈ 𝑖𝑖 ≈ ( 𝑎𝑆 ) ) → ( 𝑗𝑆 ) ≈ ( 𝑎𝑆 ) )
4 2 3 sylan2 ( ( ( 𝑗𝑆 ) ≈ 𝑖 ∧ ( 𝑎𝑆 ) ≈ 𝑖 ) → ( 𝑗𝑆 ) ≈ ( 𝑎𝑆 ) )
5 simpl ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → 𝑆 ⊆ ω )
6 simprl ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → 𝑗𝑆 )
7 5 6 sseldd ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → 𝑗 ∈ ω )
8 nnfi ( 𝑗 ∈ ω → 𝑗 ∈ Fin )
9 inss1 ( 𝑗𝑆 ) ⊆ 𝑗
10 ssfi ( ( 𝑗 ∈ Fin ∧ ( 𝑗𝑆 ) ⊆ 𝑗 ) → ( 𝑗𝑆 ) ∈ Fin )
11 8 9 10 sylancl ( 𝑗 ∈ ω → ( 𝑗𝑆 ) ∈ Fin )
12 7 11 syl ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → ( 𝑗𝑆 ) ∈ Fin )
13 simprr ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → 𝑎𝑆 )
14 5 13 sseldd ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → 𝑎 ∈ ω )
15 nnfi ( 𝑎 ∈ ω → 𝑎 ∈ Fin )
16 inss1 ( 𝑎𝑆 ) ⊆ 𝑎
17 ssfi ( ( 𝑎 ∈ Fin ∧ ( 𝑎𝑆 ) ⊆ 𝑎 ) → ( 𝑎𝑆 ) ∈ Fin )
18 15 16 17 sylancl ( 𝑎 ∈ ω → ( 𝑎𝑆 ) ∈ Fin )
19 14 18 syl ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → ( 𝑎𝑆 ) ∈ Fin )
20 nnord ( 𝑗 ∈ ω → Ord 𝑗 )
21 nnord ( 𝑎 ∈ ω → Ord 𝑎 )
22 ordtri2or2 ( ( Ord 𝑗 ∧ Ord 𝑎 ) → ( 𝑗𝑎𝑎𝑗 ) )
23 20 21 22 syl2an ( ( 𝑗 ∈ ω ∧ 𝑎 ∈ ω ) → ( 𝑗𝑎𝑎𝑗 ) )
24 7 14 23 syl2anc ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → ( 𝑗𝑎𝑎𝑗 ) )
25 ssrin ( 𝑗𝑎 → ( 𝑗𝑆 ) ⊆ ( 𝑎𝑆 ) )
26 ssrin ( 𝑎𝑗 → ( 𝑎𝑆 ) ⊆ ( 𝑗𝑆 ) )
27 25 26 orim12i ( ( 𝑗𝑎𝑎𝑗 ) → ( ( 𝑗𝑆 ) ⊆ ( 𝑎𝑆 ) ∨ ( 𝑎𝑆 ) ⊆ ( 𝑗𝑆 ) ) )
28 24 27 syl ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → ( ( 𝑗𝑆 ) ⊆ ( 𝑎𝑆 ) ∨ ( 𝑎𝑆 ) ⊆ ( 𝑗𝑆 ) ) )
29 fin23lem25 ( ( ( 𝑗𝑆 ) ∈ Fin ∧ ( 𝑎𝑆 ) ∈ Fin ∧ ( ( 𝑗𝑆 ) ⊆ ( 𝑎𝑆 ) ∨ ( 𝑎𝑆 ) ⊆ ( 𝑗𝑆 ) ) ) → ( ( 𝑗𝑆 ) ≈ ( 𝑎𝑆 ) ↔ ( 𝑗𝑆 ) = ( 𝑎𝑆 ) ) )
30 12 19 28 29 syl3anc ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → ( ( 𝑗𝑆 ) ≈ ( 𝑎𝑆 ) ↔ ( 𝑗𝑆 ) = ( 𝑎𝑆 ) ) )
31 ordom Ord ω
32 fin23lem24 ( ( ( Ord ω ∧ 𝑆 ⊆ ω ) ∧ ( 𝑗𝑆𝑎𝑆 ) ) → ( ( 𝑗𝑆 ) = ( 𝑎𝑆 ) ↔ 𝑗 = 𝑎 ) )
33 31 32 mpanl1 ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → ( ( 𝑗𝑆 ) = ( 𝑎𝑆 ) ↔ 𝑗 = 𝑎 ) )
34 30 33 bitrd ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → ( ( 𝑗𝑆 ) ≈ ( 𝑎𝑆 ) ↔ 𝑗 = 𝑎 ) )
35 4 34 syl5ib ( ( 𝑆 ⊆ ω ∧ ( 𝑗𝑆𝑎𝑆 ) ) → ( ( ( 𝑗𝑆 ) ≈ 𝑖 ∧ ( 𝑎𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) )
36 35 ralrimivva ( 𝑆 ⊆ ω → ∀ 𝑗𝑆𝑎𝑆 ( ( ( 𝑗𝑆 ) ≈ 𝑖 ∧ ( 𝑎𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) )
37 36 ad2antrr ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∀ 𝑗𝑆𝑎𝑆 ( ( ( 𝑗𝑆 ) ≈ 𝑖 ∧ ( 𝑎𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) )
38 ineq1 ( 𝑗 = 𝑎 → ( 𝑗𝑆 ) = ( 𝑎𝑆 ) )
39 38 breq1d ( 𝑗 = 𝑎 → ( ( 𝑗𝑆 ) ≈ 𝑖 ↔ ( 𝑎𝑆 ) ≈ 𝑖 ) )
40 39 reu4 ( ∃! 𝑗𝑆 ( 𝑗𝑆 ) ≈ 𝑖 ↔ ( ∃ 𝑗𝑆 ( 𝑗𝑆 ) ≈ 𝑖 ∧ ∀ 𝑗𝑆𝑎𝑆 ( ( ( 𝑗𝑆 ) ≈ 𝑖 ∧ ( 𝑎𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) ) )
41 1 37 40 sylanbrc ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∃! 𝑗𝑆 ( 𝑗𝑆 ) ≈ 𝑖 )