ackbij1lem15

		Ref	Expression
	Hypothesis	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	Assertion	ackbij1lem15	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to \neg F (A \cap suc c) = F (B \cap suc c)$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2		simpr1	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to c \in ω$
3		ackbij1lem3	$⊢ c \in ω \to c \in (𝒫 ω \cap Fin)$
4	2 3	syl	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to c \in (𝒫 ω \cap Fin)$
5		simpr3	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to \neg c \in B$
6		ackbij1lem1	$⊢ \neg c \in B \to B \cap suc c = B \cap c$
7	5 6	syl	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to B \cap suc c = B \cap c$
8		inss2	$⊢ B \cap c \subseteq c$
9	7 8	eqsstrdi	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to B \cap suc c \subseteq c$
10	1	ackbij1lem12	$⊢ (c \in (𝒫 ω \cap Fin) \land B \cap suc c \subseteq c) \to F (B \cap suc c) \subseteq F (c)$
11	4 9 10	syl2anc	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to F (B \cap suc c) \subseteq F (c)$
12	1	ackbij1lem10	$⊢ F : 𝒫 ω \cap Fin ⟶ ω$
13	12	ffvelcdmi	$⊢ c \in (𝒫 ω \cap Fin) \to F (c) \in ω$
14		nnon	$⊢ F (c) \in ω \to F (c) \in On$
15		onpsssuc	$⊢ F (c) \in On \to F (c) \subset suc F (c)$
16	4 13 14 15	4syl	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to F (c) \subset suc F (c)$
17	1	ackbij1lem14	$⊢ c \in ω \to F (\{c\}) = suc F (c)$
18	2 17	syl	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to F (\{c\}) = suc F (c)$
19	18	psseq2d	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to (F (c) \subset F (\{c\}) \leftrightarrow F (c) \subset suc F (c))$
20	16 19	mpbird	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to F (c) \subset F (\{c\})$
21		simpll	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to A \in (𝒫 ω \cap Fin)$
22		inss1	$⊢ A \cap suc c \subseteq A$
23	1	ackbij1lem11	$⊢ (A \in (𝒫 ω \cap Fin) \land A \cap suc c \subseteq A) \to A \cap suc c \in (𝒫 ω \cap Fin)$
24	21 22 23	sylancl	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to A \cap suc c \in (𝒫 ω \cap Fin)$
25		ssun1	$⊢ \{c\} \subseteq \{c\} \cup (A \cap c)$
26		simpr2	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to c \in A$
27		ackbij1lem2	$⊢ c \in A \to A \cap suc c = \{c\} \cup (A \cap c)$
28	26 27	syl	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to A \cap suc c = \{c\} \cup (A \cap c)$
29	25 28	sseqtrrid	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to \{c\} \subseteq A \cap suc c$
30	1	ackbij1lem12	$⊢ (A \cap suc c \in (𝒫 ω \cap Fin) \land \{c\} \subseteq A \cap suc c) \to F (\{c\}) \subseteq F (A \cap suc c)$
31	24 29 30	syl2anc	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to F (\{c\}) \subseteq F (A \cap suc c)$
32	20 31	psssstrd	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to F (c) \subset F (A \cap suc c)$
33	11 32	sspsstrd	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to F (B \cap suc c) \subset F (A \cap suc c)$
34	33	pssned	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to F (B \cap suc c) \neq F (A \cap suc c)$
35	34	necomd	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to F (A \cap suc c) \neq F (B \cap suc c)$
36	35	neneqd	$⊢ ((A \in (𝒫 ω \cap Fin) \land B \in (𝒫 ω \cap Fin)) \land (c \in ω \land c \in A \land \neg c \in B)) \to \neg F (A \cap suc c) = F (B \cap suc c)$

Metamath Proof Explorer

Theorem ackbij1lem15

Proof