Metamath Proof Explorer


Theorem ackbij1lem15

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

Ref Expression
Hypothesis ackbij.f 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ 𝑦𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion ackbij1lem15 ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ¬ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) )

Proof

Step Hyp Ref Expression
1 ackbij.f 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ 𝑦𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 simpr1 ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → 𝑐 ∈ ω )
3 ackbij1lem3 ( 𝑐 ∈ ω → 𝑐 ∈ ( 𝒫 ω ∩ Fin ) )
4 2 3 syl ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → 𝑐 ∈ ( 𝒫 ω ∩ Fin ) )
5 simpr3 ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ¬ 𝑐𝐵 )
6 ackbij1lem1 ( ¬ 𝑐𝐵 → ( 𝐵 ∩ suc 𝑐 ) = ( 𝐵𝑐 ) )
7 5 6 syl ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐵 ∩ suc 𝑐 ) = ( 𝐵𝑐 ) )
8 inss2 ( 𝐵𝑐 ) ⊆ 𝑐
9 7 8 eqsstrdi ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐵 ∩ suc 𝑐 ) ⊆ 𝑐 )
10 1 ackbij1lem12 ( ( 𝑐 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐵 ∩ suc 𝑐 ) ⊆ 𝑐 ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ⊆ ( 𝐹𝑐 ) )
11 4 9 10 syl2anc ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ⊆ ( 𝐹𝑐 ) )
12 1 ackbij1lem10 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω
13 12 ffvelrni ( 𝑐 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹𝑐 ) ∈ ω )
14 nnon ( ( 𝐹𝑐 ) ∈ ω → ( 𝐹𝑐 ) ∈ On )
15 onpsssuc ( ( 𝐹𝑐 ) ∈ On → ( 𝐹𝑐 ) ⊊ suc ( 𝐹𝑐 ) )
16 4 13 14 15 4syl ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐹𝑐 ) ⊊ suc ( 𝐹𝑐 ) )
17 1 ackbij1lem14 ( 𝑐 ∈ ω → ( 𝐹 ‘ { 𝑐 } ) = suc ( 𝐹𝑐 ) )
18 2 17 syl ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐹 ‘ { 𝑐 } ) = suc ( 𝐹𝑐 ) )
19 18 psseq2d ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( ( 𝐹𝑐 ) ⊊ ( 𝐹 ‘ { 𝑐 } ) ↔ ( 𝐹𝑐 ) ⊊ suc ( 𝐹𝑐 ) ) )
20 16 19 mpbird ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐹𝑐 ) ⊊ ( 𝐹 ‘ { 𝑐 } ) )
21 simpll ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → 𝐴 ∈ ( 𝒫 ω ∩ Fin ) )
22 inss1 ( 𝐴 ∩ suc 𝑐 ) ⊆ 𝐴
23 1 ackbij1lem11 ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ suc 𝑐 ) ⊆ 𝐴 ) → ( 𝐴 ∩ suc 𝑐 ) ∈ ( 𝒫 ω ∩ Fin ) )
24 21 22 23 sylancl ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐴 ∩ suc 𝑐 ) ∈ ( 𝒫 ω ∩ Fin ) )
25 ssun1 { 𝑐 } ⊆ ( { 𝑐 } ∪ ( 𝐴𝑐 ) )
26 simpr2 ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → 𝑐𝐴 )
27 ackbij1lem2 ( 𝑐𝐴 → ( 𝐴 ∩ suc 𝑐 ) = ( { 𝑐 } ∪ ( 𝐴𝑐 ) ) )
28 26 27 syl ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐴 ∩ suc 𝑐 ) = ( { 𝑐 } ∪ ( 𝐴𝑐 ) ) )
29 25 28 sseqtrrid ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → { 𝑐 } ⊆ ( 𝐴 ∩ suc 𝑐 ) )
30 1 ackbij1lem12 ( ( ( 𝐴 ∩ suc 𝑐 ) ∈ ( 𝒫 ω ∩ Fin ) ∧ { 𝑐 } ⊆ ( 𝐴 ∩ suc 𝑐 ) ) → ( 𝐹 ‘ { 𝑐 } ) ⊆ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) )
31 24 29 30 syl2anc ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐹 ‘ { 𝑐 } ) ⊆ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) )
32 20 31 psssstrd ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐹𝑐 ) ⊊ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) )
33 11 32 sspsstrd ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ⊊ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) )
34 33 pssned ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) ≠ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) )
35 34 necomd ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) ≠ ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) )
36 35 neneqd ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) ∧ ( 𝑐 ∈ ω ∧ 𝑐𝐴 ∧ ¬ 𝑐𝐵 ) ) → ¬ ( 𝐹 ‘ ( 𝐴 ∩ suc 𝑐 ) ) = ( 𝐹 ‘ ( 𝐵 ∩ suc 𝑐 ) ) )