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

Metamath Proof Explorer

Theorem canthp1lem2

Proof