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 imbitrid ⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) )
36 35 ralrimivva ⊢ ( 𝑆 ⊆ ω → ∀ 𝑗 ∈ 𝑆 ∀ 𝑎 ∈ 𝑆 ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) )
37 36 ad2antrr ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∀ 𝑗 ∈ 𝑆 ∀ 𝑎 ∈ 𝑆 ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) )
38 ineq1 ⊢ ( 𝑗 = 𝑎 → ( 𝑗 ∩ 𝑆 ) = ( 𝑎 ∩ 𝑆 ) )
39 38 breq1d ⊢ ( 𝑗 = 𝑎 → ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ↔ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) )
40 39 reu4 ⊢ ( ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ↔ ( ∃ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ∀ 𝑗 ∈ 𝑆 ∀ 𝑎 ∈ 𝑆 ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) ) )
41 1 37 40 sylanbrc ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 )