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 𝑐 ) ) )