canthnumlem

	Ref	Expression
Hypotheses	canth4.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\}$
	canth4.2	$⊢ B = ⋃ dom W$
	canth4.3	$⊢ C = {W (B)}^{-1} [\{F (B)\}]$
Assertion	canthnumlem	$⊢ A \in V \to \neg F : 𝒫 A \cap dom card \underset{1-1}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		canth4.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\}$
2		canth4.2	$⊢ B = ⋃ dom W$
3		canth4.3	$⊢ C = {W (B)}^{-1} [\{F (B)\}]$
4		f1f	$⊢ F : 𝒫 A \cap dom card \underset{1-1}{⟶} A \to F : 𝒫 A \cap dom card ⟶ A$
5		ssid	$⊢ 𝒫 A \cap dom card \subseteq 𝒫 A \cap dom card$
6	1 2 3	canth4	$⊢ (A \in V \land F : 𝒫 A \cap dom card ⟶ A \land 𝒫 A \cap dom card \subseteq 𝒫 A \cap dom card) \to (B \subseteq A \land C \subset B \land F (B) = F (C))$
7	5 6	mp3an3	$⊢ (A \in V \land F : 𝒫 A \cap dom card ⟶ A) \to (B \subseteq A \land C \subset B \land F (B) = F (C))$
8	4 7	sylan2	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to (B \subseteq A \land C \subset B \land F (B) = F (C))$
9	8	simp3d	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to F (B) = F (C)$
10		simpr	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to F : 𝒫 A \cap dom card \underset{1-1}{⟶} A$
11	8	simp1d	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to B \subseteq A$
12		elpw2g	$⊢ A \in V \to (B \in 𝒫 A \leftrightarrow B \subseteq A)$
13	12	adantr	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to (B \in 𝒫 A \leftrightarrow B \subseteq A)$
14	11 13	mpbird	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to B \in 𝒫 A$
15		eqid	$⊢ B = B$
16		eqid	$⊢ W (B) = W (B)$
17	15 16	pm3.2i	$⊢ (B = B \land W (B) = W (B))$
18		simpl	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to A \in V$
19	10 4	syl	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to F : 𝒫 A \cap dom card ⟶ A$
20	19	ffvelcdmda	$⊢ ((A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \land x \in (𝒫 A \cap dom card)) \to F (x) \in A$
21	1 18 20 2	fpwwe	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to ((B W W (B) \land F (B) \in B) \leftrightarrow (B = B \land W (B) = W (B)))$
22	17 21	mpbiri	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to (B W W (B) \land F (B) \in B)$
23	22	simpld	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to B W W (B)$
24	1 18	fpwwelem	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to (B W W (B) \leftrightarrow ((B \subseteq A \land W (B) \subseteq B \times B) \land (W (B) We B \land \forall y \in B F ({W (B)}^{-1} [\{y\}]) = y)))$
25	23 24	mpbid	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to ((B \subseteq A \land W (B) \subseteq B \times B) \land (W (B) We B \land \forall y \in B F ({W (B)}^{-1} [\{y\}]) = y))$
26	25	simprld	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to W (B) We B$
27		fvex	$⊢ W (B) \in V$
28		weeq1	$⊢ r = W (B) \to (r We B \leftrightarrow W (B) We B)$
29	27 28	spcev	$⊢ W (B) We B \to \exists r r We B$
30	26 29	syl	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to \exists r r We B$
31		ween	$⊢ B \in dom card \leftrightarrow \exists r r We B$
32	30 31	sylibr	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to B \in dom card$
33	14 32	elind	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to B \in (𝒫 A \cap dom card)$
34	8	simp2d	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to C \subset B$
35	34	pssssd	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to C \subseteq B$
36	35 11	sstrd	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to C \subseteq A$
37		elpw2g	$⊢ A \in V \to (C \in 𝒫 A \leftrightarrow C \subseteq A)$
38	37	adantr	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to (C \in 𝒫 A \leftrightarrow C \subseteq A)$
39	36 38	mpbird	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to C \in 𝒫 A$
40		ssnum	$⊢ (B \in dom card \land C \subseteq B) \to C \in dom card$
41	32 35 40	syl2anc	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to C \in dom card$
42	39 41	elind	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to C \in (𝒫 A \cap dom card)$
43		f1fveq	$⊢ (F : 𝒫 A \cap dom card \underset{1-1}{⟶} A \land (B \in (𝒫 A \cap dom card) \land C \in (𝒫 A \cap dom card))) \to (F (B) = F (C) \leftrightarrow B = C)$
44	10 33 42 43	syl12anc	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to (F (B) = F (C) \leftrightarrow B = C)$
45	9 44	mpbid	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to B = C$
46	34	pssned	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to C \neq B$
47	46	necomd	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to B \neq C$
48	47	neneqd	$⊢ (A \in V \land F : 𝒫 A \cap dom card \underset{1-1}{⟶} A) \to \neg B = C$
49	45 48	pm2.65da	$⊢ A \in V \to \neg F : 𝒫 A \cap dom card \underset{1-1}{⟶} A$

Metamath Proof Explorer

Theorem canthnumlem

Proof