canthp1lem2

	Ref	Expression
Hypotheses	canthp1lem2.1	$⊢ φ \to 1_{𝑜} ≺ A$
	canthp1lem2.2	$⊢ φ \to F : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})$
	canthp1lem2.3	$⊢ φ \to G : (A ⊔︀ 1_{𝑜}) ∖ \{F (A)\} \underset{1-1 onto}{⟶} A$
	canthp1lem2.4	$⊢ H = (G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))$
	canthp1lem2.5	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x H (r^{-1} [\{y\}]) = y))\}$
	canthp1lem2.6	$⊢ B = ⋃ dom W$
Assertion	canthp1lem2	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		canthp1lem2.1	$⊢ φ \to 1_{𝑜} ≺ A$
2		canthp1lem2.2	$⊢ φ \to F : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})$
3		canthp1lem2.3	$⊢ φ \to G : (A ⊔︀ 1_{𝑜}) ∖ \{F (A)\} \underset{1-1 onto}{⟶} A$
4		canthp1lem2.4	$⊢ H = (G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))$
5		canthp1lem2.5	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x H (r^{-1} [\{y\}]) = y))\}$
6		canthp1lem2.6	$⊢ B = ⋃ dom W$
7		relsdom	$⊢ Rel ≺$
8	7	brrelex2i	$⊢ 1_{𝑜} ≺ A \to A \in V$
9	1 8	syl	$⊢ φ \to A \in V$
10	9	pwexd	$⊢ φ \to 𝒫 A \in V$
11		f1oeng	$⊢ (𝒫 A \in V \land F : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜})) \to 𝒫 A \approx (A ⊔︀ 1_{𝑜})$
12	10 2 11	syl2anc	$⊢ φ \to 𝒫 A \approx (A ⊔︀ 1_{𝑜})$
13	12	ensymd	$⊢ φ \to (A ⊔︀ 1_{𝑜}) \approx 𝒫 A$
14		canth2g	$⊢ A \in V \to A ≺ 𝒫 A$
15	9 14	syl	$⊢ φ \to A ≺ 𝒫 A$
16		sdomen2	$⊢ 𝒫 A \approx (A ⊔︀ 1_{𝑜}) \to (A ≺ 𝒫 A \leftrightarrow A ≺ (A ⊔︀ 1_{𝑜}))$
17	12 16	syl	$⊢ φ \to (A ≺ 𝒫 A \leftrightarrow A ≺ (A ⊔︀ 1_{𝑜}))$
18	15 17	mpbid	$⊢ φ \to A ≺ (A ⊔︀ 1_{𝑜})$
19		sdomnen	$⊢ A ≺ (A ⊔︀ 1_{𝑜}) \to \neg A \approx (A ⊔︀ 1_{𝑜})$
20	18 19	syl	$⊢ φ \to \neg A \approx (A ⊔︀ 1_{𝑜})$
21		omelon	$⊢ ω \in On$
22		onenon	$⊢ ω \in On \to ω \in dom card$
23	21 22	ax-mp	$⊢ ω \in dom card$
24		dff1o3	$⊢ F : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) \leftrightarrow (F : 𝒫 A \underset{onto}{⟶} (A ⊔︀ 1_{𝑜}) \land Fun F^{-1})$
25	24	simprbi	$⊢ F : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) \to Fun F^{-1}$
26	2 25	syl	$⊢ φ \to Fun F^{-1}$
27		f1ofo	$⊢ F : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) \to F : 𝒫 A \underset{onto}{⟶} (A ⊔︀ 1_{𝑜})$
28	2 27	syl	$⊢ φ \to F : 𝒫 A \underset{onto}{⟶} (A ⊔︀ 1_{𝑜})$
29		f1ofn	$⊢ F : 𝒫 A \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) \to F Fn 𝒫 A$
30		fnresdm	$⊢ F Fn 𝒫 A \to {F ↾}_{𝒫 A} = F$
31		foeq1	$⊢ {F ↾}_{𝒫 A} = F \to (({F ↾}_{𝒫 A}) : 𝒫 A \underset{onto}{⟶} (A ⊔︀ 1_{𝑜}) \leftrightarrow F : 𝒫 A \underset{onto}{⟶} (A ⊔︀ 1_{𝑜}))$
32	2 29 30 31	4syl	$⊢ φ \to (({F ↾}_{𝒫 A}) : 𝒫 A \underset{onto}{⟶} (A ⊔︀ 1_{𝑜}) \leftrightarrow F : 𝒫 A \underset{onto}{⟶} (A ⊔︀ 1_{𝑜}))$
33	28 32	mpbird	$⊢ φ \to ({F ↾}_{𝒫 A}) : 𝒫 A \underset{onto}{⟶} (A ⊔︀ 1_{𝑜})$
34		fvex	$⊢ F (A) \in V$
35		f1osng	$⊢ (A \in V \land F (A) \in V) \to \{⟨A, F (A)⟩\} : \{A\} \underset{1-1 onto}{⟶} \{F (A)\}$
36	9 34 35	sylancl	$⊢ φ \to \{⟨A, F (A)⟩\} : \{A\} \underset{1-1 onto}{⟶} \{F (A)\}$
37	2 29	syl	$⊢ φ \to F Fn 𝒫 A$
38		pwidg	$⊢ A \in V \to A \in 𝒫 A$
39	9 38	syl	$⊢ φ \to A \in 𝒫 A$
40		fnressn	$⊢ (F Fn 𝒫 A \land A \in 𝒫 A) \to {F ↾}_{\{A\}} = \{⟨A, F (A)⟩\}$
41	37 39 40	syl2anc	$⊢ φ \to {F ↾}_{\{A\}} = \{⟨A, F (A)⟩\}$
42	41	f1oeq1d	$⊢ φ \to (({F ↾}_{\{A\}}) : \{A\} \underset{1-1 onto}{⟶} \{F (A)\} \leftrightarrow \{⟨A, F (A)⟩\} : \{A\} \underset{1-1 onto}{⟶} \{F (A)\})$
43	36 42	mpbird	$⊢ φ \to ({F ↾}_{\{A\}}) : \{A\} \underset{1-1 onto}{⟶} \{F (A)\}$
44		f1ofo	$⊢ ({F ↾}_{\{A\}}) : \{A\} \underset{1-1 onto}{⟶} \{F (A)\} \to ({F ↾}_{\{A\}}) : \{A\} \underset{onto}{⟶} \{F (A)\}$
45	43 44	syl	$⊢ φ \to ({F ↾}_{\{A\}}) : \{A\} \underset{onto}{⟶} \{F (A)\}$
46		resdif	$⊢ (Fun F^{-1} \land ({F ↾}_{𝒫 A}) : 𝒫 A \underset{onto}{⟶} (A ⊔︀ 1_{𝑜}) \land ({F ↾}_{\{A\}}) : \{A\} \underset{onto}{⟶} \{F (A)\}) \to ({F ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) ∖ \{F (A)\}$
47	26 33 45 46	syl3anc	$⊢ φ \to ({F ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) ∖ \{F (A)\}$
48		f1oco	$⊢ (G : (A ⊔︀ 1_{𝑜}) ∖ \{F (A)\} \underset{1-1 onto}{⟶} A \land ({F ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} (A ⊔︀ 1_{𝑜}) ∖ \{F (A)\}) \to (G \circ ({F ↾}_{(𝒫 A ∖ \{A\})})) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} A$
49	3 47 48	syl2anc	$⊢ φ \to (G \circ ({F ↾}_{(𝒫 A ∖ \{A\})})) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} A$
50		resco	$⊢ {(G \circ F) ↾}_{(𝒫 A ∖ \{A\})} = G \circ ({F ↾}_{(𝒫 A ∖ \{A\})})$
51		f1oeq1	$⊢ {(G \circ F) ↾}_{(𝒫 A ∖ \{A\})} = G \circ ({F ↾}_{(𝒫 A ∖ \{A\})}) \to (({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} A \leftrightarrow (G \circ ({F ↾}_{(𝒫 A ∖ \{A\})})) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} A)$
52	50 51	ax-mp	$⊢ ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} A \leftrightarrow (G \circ ({F ↾}_{(𝒫 A ∖ \{A\})})) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} A$
53	49 52	sylibr	$⊢ φ \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} A$
54		f1of	$⊢ ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} A \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} ⟶ A$
55	53 54	syl	$⊢ φ \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} ⟶ A$
56		0elpw	$⊢ \emptyset \in 𝒫 A$
57	56	a1i	$⊢ ((φ \land x \in 𝒫 A) \land x = A) \to \emptyset \in 𝒫 A$
58		sdom0	$⊢ \neg 1_{𝑜} ≺ \emptyset$
59		breq2	$⊢ \emptyset = A \to (1_{𝑜} ≺ \emptyset \leftrightarrow 1_{𝑜} ≺ A)$
60	58 59	mtbii	$⊢ \emptyset = A \to \neg 1_{𝑜} ≺ A$
61	60	necon2ai	$⊢ 1_{𝑜} ≺ A \to \emptyset \neq A$
62	1 61	syl	$⊢ φ \to \emptyset \neq A$
63	62	ad2antrr	$⊢ ((φ \land x \in 𝒫 A) \land x = A) \to \emptyset \neq A$
64		eldifsn	$⊢ \emptyset \in (𝒫 A ∖ \{A\}) \leftrightarrow (\emptyset \in 𝒫 A \land \emptyset \neq A)$
65	57 63 64	sylanbrc	$⊢ ((φ \land x \in 𝒫 A) \land x = A) \to \emptyset \in (𝒫 A ∖ \{A\})$
66		simplr	$⊢ ((φ \land x \in 𝒫 A) \land \neg x = A) \to x \in 𝒫 A$
67		simpr	$⊢ ((φ \land x \in 𝒫 A) \land \neg x = A) \to \neg x = A$
68	67	neqned	$⊢ ((φ \land x \in 𝒫 A) \land \neg x = A) \to x \neq A$
69		eldifsn	$⊢ x \in (𝒫 A ∖ \{A\}) \leftrightarrow (x \in 𝒫 A \land x \neq A)$
70	66 68 69	sylanbrc	$⊢ ((φ \land x \in 𝒫 A) \land \neg x = A) \to x \in (𝒫 A ∖ \{A\})$
71	65 70	ifclda	$⊢ (φ \land x \in 𝒫 A) \to if (x = A, \emptyset, x) \in (𝒫 A ∖ \{A\})$
72	71	fmpttd	$⊢ φ \to (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) : 𝒫 A ⟶ 𝒫 A ∖ \{A\}$
73	55 72	fcod	$⊢ φ \to (({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))) : 𝒫 A ⟶ A$
74	72	frnd	$⊢ φ \to ran (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) \subseteq 𝒫 A ∖ \{A\}$
75		cores	$⊢ ran (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) \subseteq 𝒫 A ∖ \{A\} \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) = (G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))$
76	74 75	syl	$⊢ φ \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) = (G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))$
77	76 4	eqtr4di	$⊢ φ \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) = H$
78	77	feq1d	$⊢ φ \to ((({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))) : 𝒫 A ⟶ A \leftrightarrow H : 𝒫 A ⟶ A)$
79	73 78	mpbid	$⊢ φ \to H : 𝒫 A ⟶ A$
80		inss1	$⊢ 𝒫 A \cap dom card \subseteq 𝒫 A$
81	80	a1i	$⊢ φ \to 𝒫 A \cap dom card \subseteq 𝒫 A$
82		eqid	$⊢ {W (B)}^{-1} [\{H (B)\}] = {W (B)}^{-1} [\{H (B)\}]$
83	5 6 82	canth4	$⊢ (A \in V \land H : 𝒫 A ⟶ A \land 𝒫 A \cap dom card \subseteq 𝒫 A) \to (B \subseteq A \land {W (B)}^{-1} [\{H (B)\}] \subset B \land H (B) = H ({W (B)}^{-1} [\{H (B)\}]))$
84	9 79 81 83	syl3anc	$⊢ φ \to (B \subseteq A \land {W (B)}^{-1} [\{H (B)\}] \subset B \land H (B) = H ({W (B)}^{-1} [\{H (B)\}]))$
85	84	simp1d	$⊢ φ \to B \subseteq A$
86	84	simp2d	$⊢ φ \to {W (B)}^{-1} [\{H (B)\}] \subset B$
87	86	pssned	$⊢ φ \to {W (B)}^{-1} [\{H (B)\}] \neq B$
88	87	necomd	$⊢ φ \to B \neq {W (B)}^{-1} [\{H (B)\}]$
89	84	simp3d	$⊢ φ \to H (B) = H ({W (B)}^{-1} [\{H (B)\}])$
90	4	fveq1i	$⊢ H (B) = ((G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))) (B)$
91	4	fveq1i	$⊢ H ({W (B)}^{-1} [\{H (B)\}]) = ((G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))) ({W (B)}^{-1} [\{H (B)\}])$
92	89 90 91	3eqtr3g	$⊢ φ \to ((G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))) (B) = ((G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))) ({W (B)}^{-1} [\{H (B)\}])$
93	9 85	sselpwd	$⊢ φ \to B \in 𝒫 A$
94	72 93	fvco3d	$⊢ φ \to ((G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))) (B) = (G \circ F) ((x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) (B))$
95	86	pssssd	$⊢ φ \to {W (B)}^{-1} [\{H (B)\}] \subseteq B$
96	95 85	sstrd	$⊢ φ \to {W (B)}^{-1} [\{H (B)\}] \subseteq A$
97	9 96	sselpwd	$⊢ φ \to {W (B)}^{-1} [\{H (B)\}] \in 𝒫 A$
98	72 97	fvco3d	$⊢ φ \to ((G \circ F) \circ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))) ({W (B)}^{-1} [\{H (B)\}]) = (G \circ F) ((x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) ({W (B)}^{-1} [\{H (B)\}]))$
99	92 94 98	3eqtr3d	$⊢ φ \to (G \circ F) ((x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) (B)) = (G \circ F) ((x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) ({W (B)}^{-1} [\{H (B)\}]))$
100	99	adantr	$⊢ (φ \land B \subset A) \to (G \circ F) ((x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) (B)) = (G \circ F) ((x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) ({W (B)}^{-1} [\{H (B)\}]))$
101		eqid	$⊢ (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) = (x \in 𝒫 A ⟼ if (x = A, \emptyset, x))$
102		eqeq1	$⊢ x = B \to (x = A \leftrightarrow B = A)$
103		id	$⊢ x = B \to x = B$
104	102 103	ifbieq2d	$⊢ x = B \to if (x = A, \emptyset, x) = if (B = A, \emptyset, B)$
105		ifcl	$⊢ (\emptyset \in 𝒫 A \land B \in 𝒫 A) \to if (B = A, \emptyset, B) \in 𝒫 A$
106	56 93 105	sylancr	$⊢ φ \to if (B = A, \emptyset, B) \in 𝒫 A$
107	101 104 93 106	fvmptd3	$⊢ φ \to (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) (B) = if (B = A, \emptyset, B)$
108		pssne	$⊢ B \subset A \to B \neq A$
109	108	neneqd	$⊢ B \subset A \to \neg B = A$
110	109	iffalsed	$⊢ B \subset A \to if (B = A, \emptyset, B) = B$
111	107 110	sylan9eq	$⊢ (φ \land B \subset A) \to (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) (B) = B$
112	111	fveq2d	$⊢ (φ \land B \subset A) \to (G \circ F) ((x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) (B)) = (G \circ F) (B)$
113		eqeq1	$⊢ x = {W (B)}^{-1} [\{H (B)\}] \to (x = A \leftrightarrow {W (B)}^{-1} [\{H (B)\}] = A)$
114		id	$⊢ x = {W (B)}^{-1} [\{H (B)\}] \to x = {W (B)}^{-1} [\{H (B)\}]$
115	113 114	ifbieq2d	$⊢ x = {W (B)}^{-1} [\{H (B)\}] \to if (x = A, \emptyset, x) = if ({W (B)}^{-1} [\{H (B)\}] = A, \emptyset, {W (B)}^{-1} [\{H (B)\}])$
116		ifcl	$⊢ (\emptyset \in 𝒫 A \land {W (B)}^{-1} [\{H (B)\}] \in 𝒫 A) \to if ({W (B)}^{-1} [\{H (B)\}] = A, \emptyset, {W (B)}^{-1} [\{H (B)\}]) \in 𝒫 A$
117	56 97 116	sylancr	$⊢ φ \to if ({W (B)}^{-1} [\{H (B)\}] = A, \emptyset, {W (B)}^{-1} [\{H (B)\}]) \in 𝒫 A$
118	101 115 97 117	fvmptd3	$⊢ φ \to (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) ({W (B)}^{-1} [\{H (B)\}]) = if ({W (B)}^{-1} [\{H (B)\}] = A, \emptyset, {W (B)}^{-1} [\{H (B)\}])$
119	118	adantr	$⊢ (φ \land B \subset A) \to (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) ({W (B)}^{-1} [\{H (B)\}]) = if ({W (B)}^{-1} [\{H (B)\}] = A, \emptyset, {W (B)}^{-1} [\{H (B)\}])$
120		sspsstr	$⊢ ({W (B)}^{-1} [\{H (B)\}] \subseteq B \land B \subset A) \to {W (B)}^{-1} [\{H (B)\}] \subset A$
121	95 120	sylan	$⊢ (φ \land B \subset A) \to {W (B)}^{-1} [\{H (B)\}] \subset A$
122	121	pssned	$⊢ (φ \land B \subset A) \to {W (B)}^{-1} [\{H (B)\}] \neq A$
123	122	neneqd	$⊢ (φ \land B \subset A) \to \neg {W (B)}^{-1} [\{H (B)\}] = A$
124	123	iffalsed	$⊢ (φ \land B \subset A) \to if ({W (B)}^{-1} [\{H (B)\}] = A, \emptyset, {W (B)}^{-1} [\{H (B)\}]) = {W (B)}^{-1} [\{H (B)\}]$
125	119 124	eqtrd	$⊢ (φ \land B \subset A) \to (x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) ({W (B)}^{-1} [\{H (B)\}]) = {W (B)}^{-1} [\{H (B)\}]$
126	125	fveq2d	$⊢ (φ \land B \subset A) \to (G \circ F) ((x \in 𝒫 A ⟼ if (x = A, \emptyset, x)) ({W (B)}^{-1} [\{H (B)\}])) = (G \circ F) ({W (B)}^{-1} [\{H (B)\}])$
127	100 112 126	3eqtr3d	$⊢ (φ \land B \subset A) \to (G \circ F) (B) = (G \circ F) ({W (B)}^{-1} [\{H (B)\}])$
128	93 108	anim12i	$⊢ (φ \land B \subset A) \to (B \in 𝒫 A \land B \neq A)$
129		eldifsn	$⊢ B \in (𝒫 A ∖ \{A\}) \leftrightarrow (B \in 𝒫 A \land B \neq A)$
130	128 129	sylibr	$⊢ (φ \land B \subset A) \to B \in (𝒫 A ∖ \{A\})$
131	130	fvresd	$⊢ (φ \land B \subset A) \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) (B) = (G \circ F) (B)$
132	97	adantr	$⊢ (φ \land B \subset A) \to {W (B)}^{-1} [\{H (B)\}] \in 𝒫 A$
133		eldifsn	$⊢ {W (B)}^{-1} [\{H (B)\}] \in (𝒫 A ∖ \{A\}) \leftrightarrow ({W (B)}^{-1} [\{H (B)\}] \in 𝒫 A \land {W (B)}^{-1} [\{H (B)\}] \neq A)$
134	132 122 133	sylanbrc	$⊢ (φ \land B \subset A) \to {W (B)}^{-1} [\{H (B)\}] \in (𝒫 A ∖ \{A\})$
135	134	fvresd	$⊢ (φ \land B \subset A) \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) ({W (B)}^{-1} [\{H (B)\}]) = (G \circ F) ({W (B)}^{-1} [\{H (B)\}])$
136	127 131 135	3eqtr4d	$⊢ (φ \land B \subset A) \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) (B) = ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) ({W (B)}^{-1} [\{H (B)\}])$
137		f1of1	$⊢ ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1 onto}{⟶} A \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1}{⟶} A$
138	53 137	syl	$⊢ φ \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1}{⟶} A$
139	138	adantr	$⊢ (φ \land B \subset A) \to ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1}{⟶} A$
140		f1fveq	$⊢ (({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) : 𝒫 A ∖ \{A\} \underset{1-1}{⟶} A \land (B \in (𝒫 A ∖ \{A\}) \land {W (B)}^{-1} [\{H (B)\}] \in (𝒫 A ∖ \{A\}))) \to (({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) (B) = ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) ({W (B)}^{-1} [\{H (B)\}]) \leftrightarrow B = {W (B)}^{-1} [\{H (B)\}])$
141	139 130 134 140	syl12anc	$⊢ (φ \land B \subset A) \to (({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) (B) = ({(G \circ F) ↾}_{(𝒫 A ∖ \{A\})}) ({W (B)}^{-1} [\{H (B)\}]) \leftrightarrow B = {W (B)}^{-1} [\{H (B)\}])$
142	136 141	mpbid	$⊢ (φ \land B \subset A) \to B = {W (B)}^{-1} [\{H (B)\}]$
143	142	ex	$⊢ φ \to (B \subset A \to B = {W (B)}^{-1} [\{H (B)\}])$
144	143	necon3ad	$⊢ φ \to (B \neq {W (B)}^{-1} [\{H (B)\}] \to \neg B \subset A)$
145	88 144	mpd	$⊢ φ \to \neg B \subset A$
146		npss	$⊢ \neg B \subset A \leftrightarrow (B \subseteq A \to B = A)$
147	145 146	sylib	$⊢ φ \to (B \subseteq A \to B = A)$
148	85 147	mpd	$⊢ φ \to B = A$
149		eqid	$⊢ B = B$
150		eqid	$⊢ W (B) = W (B)$
151	149 150	pm3.2i	$⊢ (B = B \land W (B) = W (B))$
152		elinel1	$⊢ x \in (𝒫 A \cap dom card) \to x \in 𝒫 A$
153		ffvelrn	$⊢ (H : 𝒫 A ⟶ A \land x \in 𝒫 A) \to H (x) \in A$
154	79 152 153	syl2an	$⊢ (φ \land x \in (𝒫 A \cap dom card)) \to H (x) \in A$
155	5 9 154 6	fpwwe	$⊢ φ \to ((B W W (B) \land H (B) \in B) \leftrightarrow (B = B \land W (B) = W (B)))$
156	151 155	mpbiri	$⊢ φ \to (B W W (B) \land H (B) \in B)$
157	156	simpld	$⊢ φ \to B W W (B)$
158	5 9	fpwwelem	$⊢ φ \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 H ({W (B)}^{-1} [\{y\}]) = y)))$
159	157 158	mpbid	$⊢ φ \to ((B \subseteq A \land W (B) \subseteq B \times B) \land (W (B) We B \land \forall y \in B H ({W (B)}^{-1} [\{y\}]) = y))$
160	159	simprld	$⊢ φ \to W (B) We B$
161		fvex	$⊢ W (B) \in V$
162		weeq1	$⊢ r = W (B) \to (r We B \leftrightarrow W (B) We B)$
163	161 162	spcev	$⊢ W (B) We B \to \exists r r We B$
164	160 163	syl	$⊢ φ \to \exists r r We B$
165		ween	$⊢ B \in dom card \leftrightarrow \exists r r We B$
166	164 165	sylibr	$⊢ φ \to B \in dom card$
167	148 166	eqeltrrd	$⊢ φ \to A \in dom card$
168		domtri2	$⊢ (ω \in dom card \land A \in dom card) \to (ω ≼ A \leftrightarrow \neg A ≺ ω)$
169	23 167 168	sylancr	$⊢ φ \to (ω ≼ A \leftrightarrow \neg A ≺ ω)$
170		infdju1	$⊢ ω ≼ A \to (A ⊔︀ 1_{𝑜}) \approx A$
171	169 170	syl6bir	$⊢ φ \to (\neg A ≺ ω \to (A ⊔︀ 1_{𝑜}) \approx A)$
172		ensym	$⊢ (A ⊔︀ 1_{𝑜}) \approx A \to A \approx (A ⊔︀ 1_{𝑜})$
173	171 172	syl6	$⊢ φ \to (\neg A ≺ ω \to A \approx (A ⊔︀ 1_{𝑜}))$
174	20 173	mt3d	$⊢ φ \to A ≺ ω$
175		2onn	$⊢ 2_{𝑜} \in ω$
176		nnsdom	$⊢ 2_{𝑜} \in ω \to 2_{𝑜} ≺ ω$
177	175 176	ax-mp	$⊢ 2_{𝑜} ≺ ω$
178		djufi	$⊢ (A ≺ ω \land 2_{𝑜} ≺ ω) \to (A ⊔︀ 2_{𝑜}) ≺ ω$
179	174 177 178	sylancl	$⊢ φ \to (A ⊔︀ 2_{𝑜}) ≺ ω$
180		isfinite	$⊢ (A ⊔︀ 2_{𝑜}) \in Fin \leftrightarrow (A ⊔︀ 2_{𝑜}) ≺ ω$
181	179 180	sylibr	$⊢ φ \to (A ⊔︀ 2_{𝑜}) \in Fin$
182		sssucid	$⊢ 1_{𝑜} \subseteq suc 1_{𝑜}$
183		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
184	182 183	sseqtrri	$⊢ 1_{𝑜} \subseteq 2_{𝑜}$
185		xpss2	$⊢ 1_{𝑜} \subseteq 2_{𝑜} \to \{1_{𝑜}\} \times 1_{𝑜} \subseteq \{1_{𝑜}\} \times 2_{𝑜}$
186	184 185	ax-mp	$⊢ \{1_{𝑜}\} \times 1_{𝑜} \subseteq \{1_{𝑜}\} \times 2_{𝑜}$
187		unss2	$⊢ \{1_{𝑜}\} \times 1_{𝑜} \subseteq \{1_{𝑜}\} \times 2_{𝑜} \to (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}) \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜})$
188	186 187	mp1i	$⊢ φ \to (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}) \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜})$
189		ssun2	$⊢ \{1_{𝑜}\} \times 2_{𝑜} \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜})$
190		1oex	$⊢ 1_{𝑜} \in V$
191	190	snid	$⊢ 1_{𝑜} \in \{1_{𝑜}\}$
192	190	sucid	$⊢ 1_{𝑜} \in suc 1_{𝑜}$
193	192 183	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
194		opelxpi	$⊢ (1_{𝑜} \in \{1_{𝑜}\} \land 1_{𝑜} \in 2_{𝑜}) \to ⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{1_{𝑜}\} \times 2_{𝑜})$
195	191 193 194	mp2an	$⊢ ⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{1_{𝑜}\} \times 2_{𝑜})$
196	189 195	sselii	$⊢ ⟨1_{𝑜}, 1_{𝑜}⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜}))$
197		1n0	$⊢ 1_{𝑜} \neq \emptyset$
198	197	neii	$⊢ \neg 1_{𝑜} = \emptyset$
199		opelxp1	$⊢ ⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{\emptyset\} \times A) \to 1_{𝑜} \in \{\emptyset\}$
200		elsni	$⊢ 1_{𝑜} \in \{\emptyset\} \to 1_{𝑜} = \emptyset$
201	199 200	syl	$⊢ ⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{\emptyset\} \times A) \to 1_{𝑜} = \emptyset$
202	198 201	mto	$⊢ \neg ⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{\emptyset\} \times A)$
203		1onn	$⊢ 1_{𝑜} \in ω$
204		nnord	$⊢ 1_{𝑜} \in ω \to Ord 1_{𝑜}$
205		ordirr	$⊢ Ord 1_{𝑜} \to \neg 1_{𝑜} \in 1_{𝑜}$
206	203 204 205	mp2b	$⊢ \neg 1_{𝑜} \in 1_{𝑜}$
207		opelxp2	$⊢ ⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{1_{𝑜}\} \times 1_{𝑜}) \to 1_{𝑜} \in 1_{𝑜}$
208	206 207	mto	$⊢ \neg ⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{1_{𝑜}\} \times 1_{𝑜})$
209	202 208	pm3.2ni	$⊢ \neg (⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{\emptyset\} \times A) \lor ⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{1_{𝑜}\} \times 1_{𝑜}))$
210		elun	$⊢ ⟨1_{𝑜}, 1_{𝑜}⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})) \leftrightarrow (⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{\emptyset\} \times A) \lor ⟨1_{𝑜}, 1_{𝑜}⟩ \in (\{1_{𝑜}\} \times 1_{𝑜}))$
211	209 210	mtbir	$⊢ \neg ⟨1_{𝑜}, 1_{𝑜}⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}))$
212		ssnelpss	$⊢ (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}) \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜}) \to ((⟨1_{𝑜}, 1_{𝑜}⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜})) \land \neg ⟨1_{𝑜}, 1_{𝑜}⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}))) \to (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}) \subset (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜}))$
213	196 211 212	mp2ani	$⊢ (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}) \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜}) \to (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}) \subset (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜})$
214	188 213	syl	$⊢ φ \to (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}) \subset (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜})$
215		df-dju	$⊢ (A ⊔︀ 1_{𝑜}) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜})$
216		df-dju	$⊢ (A ⊔︀ 2_{𝑜}) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜})$
217	215 216	psseq12i	$⊢ (A ⊔︀ 1_{𝑜}) \subset (A ⊔︀ 2_{𝑜}) \leftrightarrow (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 1_{𝑜}) \subset (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times 2_{𝑜})$
218	214 217	sylibr	$⊢ φ \to (A ⊔︀ 1_{𝑜}) \subset (A ⊔︀ 2_{𝑜})$
219		php3	$⊢ ((A ⊔︀ 2_{𝑜}) \in Fin \land (A ⊔︀ 1_{𝑜}) \subset (A ⊔︀ 2_{𝑜})) \to (A ⊔︀ 1_{𝑜}) ≺ (A ⊔︀ 2_{𝑜})$
220	181 218 219	syl2anc	$⊢ φ \to (A ⊔︀ 1_{𝑜}) ≺ (A ⊔︀ 2_{𝑜})$
221		canthp1lem1	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A$
222	1 221	syl	$⊢ φ \to (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A$
223		sdomdomtr	$⊢ ((A ⊔︀ 1_{𝑜}) ≺ (A ⊔︀ 2_{𝑜}) \land (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A) \to (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A$
224	220 222 223	syl2anc	$⊢ φ \to (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A$
225		sdomnen	$⊢ (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A \to \neg (A ⊔︀ 1_{𝑜}) \approx 𝒫 A$
226	224 225	syl	$⊢ φ \to \neg (A ⊔︀ 1_{𝑜}) \approx 𝒫 A$
227	13 226	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem canthp1lem2

Proof