isf32lem7

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

	Ref	Expression
Hypotheses	isf32lem.a	$⊢ φ \to F : ω ⟶ 𝒫 G$
	isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
	isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
	isf32lem.d	$⊢ S = \{y \in ω \| F (suc y) \subset F (y)\}$
	isf32lem.e	$⊢ J = (u \in ω ⟼ (ι v \in S \| (v \cap S) \approx u))$
	isf32lem.f	$⊢ K = (w \in S ⟼ F (w) ∖ F (suc w)) \circ J$
Assertion	isf32lem7	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to K (A) \cap K (B) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		isf32lem.a	$⊢ φ \to F : ω ⟶ 𝒫 G$
2		isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
3		isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
4		isf32lem.d	$⊢ S = \{y \in ω \| F (suc y) \subset F (y)\}$
5		isf32lem.e	$⊢ J = (u \in ω ⟼ (ι v \in S \| (v \cap S) \approx u))$
6		isf32lem.f	$⊢ K = (w \in S ⟼ F (w) ∖ F (suc w)) \circ J$
7	6	fveq1i	$⊢ K (A) = ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A)$
8	4	ssrab3	$⊢ S \subseteq ω$
9	1 2 3 4	isf32lem5	$⊢ φ \to \neg S \in Fin$
10	5	fin23lem22	$⊢ (S \subseteq ω \land \neg S \in Fin) \to J : ω \underset{1-1 onto}{⟶} S$
11	8 9 10	sylancr	$⊢ φ \to J : ω \underset{1-1 onto}{⟶} S$
12		f1of	$⊢ J : ω \underset{1-1 onto}{⟶} S \to J : ω ⟶ S$
13	11 12	syl	$⊢ φ \to J : ω ⟶ S$
14		fvco3	$⊢ (J : ω ⟶ S \land A \in ω) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A) = (w \in S ⟼ F (w) ∖ F (suc w)) (J (A))$
15	13 14	sylan	$⊢ (φ \land A \in ω) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A) = (w \in S ⟼ F (w) ∖ F (suc w)) (J (A))$
16	15	ad2ant2r	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A) = (w \in S ⟼ F (w) ∖ F (suc w)) (J (A))$
17	13	adantr	$⊢ (φ \land A \neq B) \to J : ω ⟶ S$
18		simpl	$⊢ (A \in ω \land B \in ω) \to A \in ω$
19		ffvelrn	$⊢ (J : ω ⟶ S \land A \in ω) \to J (A) \in S$
20	17 18 19	syl2an	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to J (A) \in S$
21		fveq2	$⊢ w = J (A) \to F (w) = F (J (A))$
22		suceq	$⊢ w = J (A) \to suc w = suc J (A)$
23	22	fveq2d	$⊢ w = J (A) \to F (suc w) = F (suc J (A))$
24	21 23	difeq12d	$⊢ w = J (A) \to F (w) ∖ F (suc w) = F (J (A)) ∖ F (suc J (A))$
25		eqid	$⊢ (w \in S ⟼ F (w) ∖ F (suc w)) = (w \in S ⟼ F (w) ∖ F (suc w))$
26		fvex	$⊢ F (J (A)) \in V$
27	26	difexi	$⊢ F (J (A)) ∖ F (suc J (A)) \in V$
28	24 25 27	fvmpt	$⊢ J (A) \in S \to (w \in S ⟼ F (w) ∖ F (suc w)) (J (A)) = F (J (A)) ∖ F (suc J (A))$
29	20 28	syl	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to (w \in S ⟼ F (w) ∖ F (suc w)) (J (A)) = F (J (A)) ∖ F (suc J (A))$
30	16 29	eqtrd	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A) = F (J (A)) ∖ F (suc J (A))$
31	7 30	syl5eq	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to K (A) = F (J (A)) ∖ F (suc J (A))$
32	6	fveq1i	$⊢ K (B) = ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (B)$
33		fvco3	$⊢ (J : ω ⟶ S \land B \in ω) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (B) = (w \in S ⟼ F (w) ∖ F (suc w)) (J (B))$
34	13 33	sylan	$⊢ (φ \land B \in ω) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (B) = (w \in S ⟼ F (w) ∖ F (suc w)) (J (B))$
35	34	ad2ant2rl	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (B) = (w \in S ⟼ F (w) ∖ F (suc w)) (J (B))$
36		simpr	$⊢ (A \in ω \land B \in ω) \to B \in ω$
37		ffvelrn	$⊢ (J : ω ⟶ S \land B \in ω) \to J (B) \in S$
38	17 36 37	syl2an	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to J (B) \in S$
39		fveq2	$⊢ w = J (B) \to F (w) = F (J (B))$
40		suceq	$⊢ w = J (B) \to suc w = suc J (B)$
41	40	fveq2d	$⊢ w = J (B) \to F (suc w) = F (suc J (B))$
42	39 41	difeq12d	$⊢ w = J (B) \to F (w) ∖ F (suc w) = F (J (B)) ∖ F (suc J (B))$
43		fvex	$⊢ F (J (B)) \in V$
44	43	difexi	$⊢ F (J (B)) ∖ F (suc J (B)) \in V$
45	42 25 44	fvmpt	$⊢ J (B) \in S \to (w \in S ⟼ F (w) ∖ F (suc w)) (J (B)) = F (J (B)) ∖ F (suc J (B))$
46	38 45	syl	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to (w \in S ⟼ F (w) ∖ F (suc w)) (J (B)) = F (J (B)) ∖ F (suc J (B))$
47	35 46	eqtrd	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (B) = F (J (B)) ∖ F (suc J (B))$
48	32 47	syl5eq	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to K (B) = F (J (B)) ∖ F (suc J (B))$
49	31 48	ineq12d	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to K (A) \cap K (B) = (F (J (A)) ∖ F (suc J (A))) \cap (F (J (B)) ∖ F (suc J (B)))$
50		simpll	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to φ$
51		simplr	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to A \neq B$
52		f1of1	$⊢ J : ω \underset{1-1 onto}{⟶} S \to J : ω \underset{1-1}{⟶} S$
53	11 52	syl	$⊢ φ \to J : ω \underset{1-1}{⟶} S$
54	53	adantr	$⊢ (φ \land A \neq B) \to J : ω \underset{1-1}{⟶} S$
55		f1fveq	$⊢ (J : ω \underset{1-1}{⟶} S \land (A \in ω \land B \in ω)) \to (J (A) = J (B) \leftrightarrow A = B)$
56	54 55	sylan	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to (J (A) = J (B) \leftrightarrow A = B)$
57	56	biimpd	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to (J (A) = J (B) \to A = B)$
58	57	necon3d	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to (A \neq B \to J (A) \neq J (B))$
59	51 58	mpd	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to J (A) \neq J (B)$
60	8 20	sseldi	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to J (A) \in ω$
61	8 38	sseldi	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to J (B) \in ω$
62	1 2 3	isf32lem4	$⊢ ((φ \land J (A) \neq J (B)) \land (J (A) \in ω \land J (B) \in ω)) \to (F (J (A)) ∖ F (suc J (A))) \cap (F (J (B)) ∖ F (suc J (B))) = \emptyset$
63	50 59 60 61 62	syl22anc	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to (F (J (A)) ∖ F (suc J (A))) \cap (F (J (B)) ∖ F (suc J (B))) = \emptyset$
64	49 63	eqtrd	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to K (A) \cap K (B) = \emptyset$

Metamath Proof Explorer

Theorem isf32lem7

Proof