Metamath Proof Explorer


Theorem isf32lem7

Description: Lemma for isfin3-2 . Different K values are disjoint. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Hypotheses isf32lem.a ( 𝜑𝐹 : ω ⟶ 𝒫 𝐺 )
isf32lem.b ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹𝑥 ) )
isf32lem.c ( 𝜑 → ¬ ran 𝐹 ∈ ran 𝐹 )
isf32lem.d 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹𝑦 ) }
isf32lem.e 𝐽 = ( 𝑢 ∈ ω ↦ ( 𝑣𝑆 ( 𝑣𝑆 ) ≈ 𝑢 ) )
isf32lem.f 𝐾 = ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 )
Assertion isf32lem7 ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐾𝐴 ) ∩ ( 𝐾𝐵 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 isf32lem.a ( 𝜑𝐹 : ω ⟶ 𝒫 𝐺 )
2 isf32lem.b ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹𝑥 ) )
3 isf32lem.c ( 𝜑 → ¬ ran 𝐹 ∈ ran 𝐹 )
4 isf32lem.d 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹𝑦 ) }
5 isf32lem.e 𝐽 = ( 𝑢 ∈ ω ↦ ( 𝑣𝑆 ( 𝑣𝑆 ) ≈ 𝑢 ) )
6 isf32lem.f 𝐾 = ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 )
7 6 fveq1i ( 𝐾𝐴 ) = ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐴 )
8 4 ssrab3 𝑆 ⊆ ω
9 1 2 3 4 isf32lem5 ( 𝜑 → ¬ 𝑆 ∈ Fin )
10 5 fin23lem22 ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → 𝐽 : ω –1-1-onto𝑆 )
11 8 9 10 sylancr ( 𝜑𝐽 : ω –1-1-onto𝑆 )
12 f1of ( 𝐽 : ω –1-1-onto𝑆𝐽 : ω ⟶ 𝑆 )
13 11 12 syl ( 𝜑𝐽 : ω ⟶ 𝑆 )
14 fvco3 ( ( 𝐽 : ω ⟶ 𝑆𝐴 ∈ ω ) → ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐴 ) = ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐴 ) ) )
15 13 14 sylan ( ( 𝜑𝐴 ∈ ω ) → ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐴 ) = ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐴 ) ) )
16 15 ad2ant2r ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐴 ) = ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐴 ) ) )
17 13 adantr ( ( 𝜑𝐴𝐵 ) → 𝐽 : ω ⟶ 𝑆 )
18 simpl ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝐴 ∈ ω )
19 ffvelrn ( ( 𝐽 : ω ⟶ 𝑆𝐴 ∈ ω ) → ( 𝐽𝐴 ) ∈ 𝑆 )
20 17 18 19 syl2an ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐽𝐴 ) ∈ 𝑆 )
21 fveq2 ( 𝑤 = ( 𝐽𝐴 ) → ( 𝐹𝑤 ) = ( 𝐹 ‘ ( 𝐽𝐴 ) ) )
22 suceq ( 𝑤 = ( 𝐽𝐴 ) → suc 𝑤 = suc ( 𝐽𝐴 ) )
23 22 fveq2d ( 𝑤 = ( 𝐽𝐴 ) → ( 𝐹 ‘ suc 𝑤 ) = ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) )
24 21 23 difeq12d ( 𝑤 = ( 𝐽𝐴 ) → ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) = ( ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) ) )
25 eqid ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) = ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) )
26 fvex ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∈ V
27 26 difexi ( ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) ) ∈ V
28 24 25 27 fvmpt ( ( 𝐽𝐴 ) ∈ 𝑆 → ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐴 ) ) = ( ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) ) )
29 20 28 syl ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐴 ) ) = ( ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) ) )
30 16 29 eqtrd ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐴 ) = ( ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) ) )
31 7 30 syl5eq ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐾𝐴 ) = ( ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) ) )
32 6 fveq1i ( 𝐾𝐵 ) = ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐵 )
33 fvco3 ( ( 𝐽 : ω ⟶ 𝑆𝐵 ∈ ω ) → ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐵 ) = ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐵 ) ) )
34 13 33 sylan ( ( 𝜑𝐵 ∈ ω ) → ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐵 ) = ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐵 ) ) )
35 34 ad2ant2rl ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐵 ) = ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐵 ) ) )
36 simpr ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝐵 ∈ ω )
37 ffvelrn ( ( 𝐽 : ω ⟶ 𝑆𝐵 ∈ ω ) → ( 𝐽𝐵 ) ∈ 𝑆 )
38 17 36 37 syl2an ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐽𝐵 ) ∈ 𝑆 )
39 fveq2 ( 𝑤 = ( 𝐽𝐵 ) → ( 𝐹𝑤 ) = ( 𝐹 ‘ ( 𝐽𝐵 ) ) )
40 suceq ( 𝑤 = ( 𝐽𝐵 ) → suc 𝑤 = suc ( 𝐽𝐵 ) )
41 40 fveq2d ( 𝑤 = ( 𝐽𝐵 ) → ( 𝐹 ‘ suc 𝑤 ) = ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) )
42 39 41 difeq12d ( 𝑤 = ( 𝐽𝐵 ) → ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) = ( ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) ) )
43 fvex ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∈ V
44 43 difexi ( ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) ) ∈ V
45 42 25 44 fvmpt ( ( 𝐽𝐵 ) ∈ 𝑆 → ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐵 ) ) = ( ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) ) )
46 38 45 syl ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽𝐵 ) ) = ( ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) ) )
47 35 46 eqtrd ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐵 ) = ( ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) ) )
48 32 47 syl5eq ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐾𝐵 ) = ( ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) ) )
49 31 48 ineq12d ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐾𝐴 ) ∩ ( 𝐾𝐵 ) ) = ( ( ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) ) ∩ ( ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) ) ) )
50 simpll ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → 𝜑 )
51 simplr ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → 𝐴𝐵 )
52 f1of1 ( 𝐽 : ω –1-1-onto𝑆𝐽 : ω –1-1𝑆 )
53 11 52 syl ( 𝜑𝐽 : ω –1-1𝑆 )
54 53 adantr ( ( 𝜑𝐴𝐵 ) → 𝐽 : ω –1-1𝑆 )
55 f1fveq ( ( 𝐽 : ω –1-1𝑆 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐽𝐴 ) = ( 𝐽𝐵 ) ↔ 𝐴 = 𝐵 ) )
56 54 55 sylan ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐽𝐴 ) = ( 𝐽𝐵 ) ↔ 𝐴 = 𝐵 ) )
57 56 biimpd ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐽𝐴 ) = ( 𝐽𝐵 ) → 𝐴 = 𝐵 ) )
58 57 necon3d ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴𝐵 → ( 𝐽𝐴 ) ≠ ( 𝐽𝐵 ) ) )
59 51 58 mpd ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐽𝐴 ) ≠ ( 𝐽𝐵 ) )
60 8 20 sseldi ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐽𝐴 ) ∈ ω )
61 8 38 sseldi ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐽𝐵 ) ∈ ω )
62 1 2 3 isf32lem4 ( ( ( 𝜑 ∧ ( 𝐽𝐴 ) ≠ ( 𝐽𝐵 ) ) ∧ ( ( 𝐽𝐴 ) ∈ ω ∧ ( 𝐽𝐵 ) ∈ ω ) ) → ( ( ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) ) ∩ ( ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) ) ) = ∅ )
63 50 59 60 61 62 syl22anc ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( ( 𝐹 ‘ ( 𝐽𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐴 ) ) ) ∩ ( ( 𝐹 ‘ ( 𝐽𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽𝐵 ) ) ) ) = ∅ )
64 49 63 eqtrd ( ( ( 𝜑𝐴𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐾𝐴 ) ∩ ( 𝐾𝐵 ) ) = ∅ )