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		ffvelcdm	⊢ ( ( 𝐽 : ω ⟶ 𝑆 ∧ 𝐴 ∈ ω ) → ( 𝐽 ‘ 𝐴 ) ∈ 𝑆 )
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	eqtrid	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐾 ‘ 𝐴 ) = ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) )
32	6	fveq1i	⊢ ( 𝐾 ‘ 𝐵 ) = ( ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐵 )
33		fvco3	⊢ ( ( 𝐽 : ω ⟶ 𝑆 ∧ 𝐵 ∈ ω ) → ( ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐵 ) = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽 ‘ 𝐵 ) ) )
34	13 33	sylan	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ω ) → ( ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐵 ) = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽 ‘ 𝐵 ) ) )
35	34	ad2ant2rl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) ‘ 𝐵 ) = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ‘ ( 𝐽 ‘ 𝐵 ) ) )
36		simpr	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝐵 ∈ ω )
37		ffvelcdm	⊢ ( ( 𝐽 : ω ⟶ 𝑆 ∧ 𝐵 ∈ ω ) → ( 𝐽 ‘ 𝐵 ) ∈ 𝑆 )
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	eqtrid	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐾 ‘ 𝐵 ) = ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐵 ) ) ∖ ( 𝐹 ‘ 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	sselid	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐽 ‘ 𝐴 ) ∈ ω )
61	8 38	sselid	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐽 ‘ 𝐵 ) ∈ ω )
62	1 2 3	isf32lem4	⊢ ( ( ( 𝜑 ∧ ( 𝐽 ‘ 𝐴 ) ≠ ( 𝐽 ‘ 𝐵 ) ) ∧ ( ( 𝐽 ‘ 𝐴 ) ∈ ω ∧ ( 𝐽 ‘ 𝐵 ) ∈ ω ) ) → ( ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) ∩ ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐵 ) ) ) ) = ∅ )
63	50 59 60 61 62	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐴 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐴 ) ) ) ∩ ( ( 𝐹 ‘ ( 𝐽 ‘ 𝐵 ) ) ∖ ( 𝐹 ‘ suc ( 𝐽 ‘ 𝐵 ) ) ) ) = ∅ )
64	49 63	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐾 ‘ 𝐴 ) ∩ ( 𝐾 ‘ 𝐵 ) ) = ∅ )

Metamath Proof Explorer

Theorem isf32lem7

Proof