topdifinffinlem

Description: This is the core of the proof of topdifinffin , but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020)

		Ref	Expression
	Hypothesis	topdifinf.t	$⊢ T = \{x \in 𝒫 A \| (\neg A ∖ x \in Fin \lor (x = \emptyset \lor x = A))\}$
	Assertion	topdifinffinlem	$⊢ T \in TopOn (A) \to A \in Fin$

Proof

Step	Hyp	Ref	Expression
1		topdifinf.t	$⊢ T = \{x \in 𝒫 A \| (\neg A ∖ x \in Fin \lor (x = \emptyset \lor x = A))\}$
2		nfv	$⊢ Ⅎ u \neg A \in Fin$
3		nfab1	$⊢ \underline{Ⅎ} u \{u \| \exists y \in A u = \{y\}\}$
4		nfcv	$⊢ \underline{Ⅎ} u T$
5		abid	$⊢ u \in \{u \| \exists y \in A u = \{y\}\} \leftrightarrow \exists y \in A u = \{y\}$
6		df-rex	$⊢ \exists y \in A u = \{y\} \leftrightarrow \exists y (y \in A \land u = \{y\})$
7	5 6	bitri	$⊢ u \in \{u \| \exists y \in A u = \{y\}\} \leftrightarrow \exists y (y \in A \land u = \{y\})$
8		eqid	$⊢ \{y\} = \{y\}$
9		snex	$⊢ \{y\} \in V$
10		snelpwi	$⊢ y \in A \to \{y\} \in 𝒫 A$
11		eleq1	$⊢ x = \{y\} \to (x \in 𝒫 A \leftrightarrow \{y\} \in 𝒫 A)$
12	10 11	syl5ibr	$⊢ x = \{y\} \to (y \in A \to x \in 𝒫 A)$
13	12	imdistani	$⊢ (x = \{y\} \land y \in A) \to (x = \{y\} \land x \in 𝒫 A)$
14	13	anim2i	$⊢ (\neg A \in Fin \land (x = \{y\} \land y \in A)) \to (\neg A \in Fin \land (x = \{y\} \land x \in 𝒫 A))$
15	14	3impb	$⊢ (\neg A \in Fin \land x = \{y\} \land y \in A) \to (\neg A \in Fin \land (x = \{y\} \land x \in 𝒫 A))$
16		3anass	$⊢ (\neg A \in Fin \land x = \{y\} \land x \in 𝒫 A) \leftrightarrow (\neg A \in Fin \land (x = \{y\} \land x \in 𝒫 A))$
17	15 16	sylibr	$⊢ (\neg A \in Fin \land x = \{y\} \land y \in A) \to (\neg A \in Fin \land x = \{y\} \land x \in 𝒫 A)$
18		snfi	$⊢ \{y\} \in Fin$
19		eleq1	$⊢ x = \{y\} \to (x \in Fin \leftrightarrow \{y\} \in Fin)$
20	18 19	mpbiri	$⊢ x = \{y\} \to x \in Fin$
21		difinf	$⊢ (\neg A \in Fin \land x \in Fin) \to \neg A ∖ x \in Fin$
22	20 21	sylan2	$⊢ (\neg A \in Fin \land x = \{y\}) \to \neg A ∖ x \in Fin$
23	22	orcd	$⊢ (\neg A \in Fin \land x = \{y\}) \to (\neg A ∖ x \in Fin \lor (x = \emptyset \lor x = A))$
24	23	anim2i	$⊢ (x \in 𝒫 A \land (\neg A \in Fin \land x = \{y\})) \to (x \in 𝒫 A \land (\neg A ∖ x \in Fin \lor (x = \emptyset \lor x = A)))$
25	24	ancoms	$⊢ ((\neg A \in Fin \land x = \{y\}) \land x \in 𝒫 A) \to (x \in 𝒫 A \land (\neg A ∖ x \in Fin \lor (x = \emptyset \lor x = A)))$
26	25	3impa	$⊢ (\neg A \in Fin \land x = \{y\} \land x \in 𝒫 A) \to (x \in 𝒫 A \land (\neg A ∖ x \in Fin \lor (x = \emptyset \lor x = A)))$
27	17 26	syl	$⊢ (\neg A \in Fin \land x = \{y\} \land y \in A) \to (x \in 𝒫 A \land (\neg A ∖ x \in Fin \lor (x = \emptyset \lor x = A)))$
28	1	rabeq2i	$⊢ x \in T \leftrightarrow (x \in 𝒫 A \land (\neg A ∖ x \in Fin \lor (x = \emptyset \lor x = A)))$
29	27 28	sylibr	$⊢ (\neg A \in Fin \land x = \{y\} \land y \in A) \to x \in T$
30		eleq1	$⊢ x = \{y\} \to (x \in T \leftrightarrow \{y\} \in T)$
31	30	3ad2ant2	$⊢ (\neg A \in Fin \land x = \{y\} \land y \in A) \to (x \in T \leftrightarrow \{y\} \in T)$
32	29 31	mpbid	$⊢ (\neg A \in Fin \land x = \{y\} \land y \in A) \to \{y\} \in T$
33	32	sbcth	$⊢ \{y\} \in V \to \underset{˙}{[} \{y\} / x \underset{˙}{]} ((\neg A \in Fin \land x = \{y\} \land y \in A) \to \{y\} \in T)$
34	9 33	ax-mp	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} ((\neg A \in Fin \land x = \{y\} \land y \in A) \to \{y\} \in T)$
35		sbcimg	$⊢ \{y\} \in V \to (\underset{˙}{[} \{y\} / x \underset{˙}{]} ((\neg A \in Fin \land x = \{y\} \land y \in A) \to \{y\} \in T) \leftrightarrow (\underset{˙}{[} \{y\} / x \underset{˙}{]} (\neg A \in Fin \land x = \{y\} \land y \in A) \to \underset{˙}{[} \{y\} / x \underset{˙}{]} \{y\} \in T))$
36	9 35	ax-mp	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} ((\neg A \in Fin \land x = \{y\} \land y \in A) \to \{y\} \in T) \leftrightarrow (\underset{˙}{[} \{y\} / x \underset{˙}{]} (\neg A \in Fin \land x = \{y\} \land y \in A) \to \underset{˙}{[} \{y\} / x \underset{˙}{]} \{y\} \in T)$
37	34 36	mpbi	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} (\neg A \in Fin \land x = \{y\} \land y \in A) \to \underset{˙}{[} \{y\} / x \underset{˙}{]} \{y\} \in T$
38		sbc3an	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} (\neg A \in Fin \land x = \{y\} \land y \in A) \leftrightarrow (\underset{˙}{[} \{y\} / x \underset{˙}{]} \neg A \in Fin \land \underset{˙}{[} \{y\} / x \underset{˙}{]} x = \{y\} \land \underset{˙}{[} \{y\} / x \underset{˙}{]} y \in A)$
39		sbcg	$⊢ \{y\} \in V \to (\underset{˙}{[} \{y\} / x \underset{˙}{]} \neg A \in Fin \leftrightarrow \neg A \in Fin)$
40	9 39	ax-mp	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} \neg A \in Fin \leftrightarrow \neg A \in Fin$
41	40	3anbi1i	$⊢ (\underset{˙}{[} \{y\} / x \underset{˙}{]} \neg A \in Fin \land \underset{˙}{[} \{y\} / x \underset{˙}{]} x = \{y\} \land \underset{˙}{[} \{y\} / x \underset{˙}{]} y \in A) \leftrightarrow (\neg A \in Fin \land \underset{˙}{[} \{y\} / x \underset{˙}{]} x = \{y\} \land \underset{˙}{[} \{y\} / x \underset{˙}{]} y \in A)$
42		eqsbc1	$⊢ \{y\} \in V \to (\underset{˙}{[} \{y\} / x \underset{˙}{]} x = \{y\} \leftrightarrow \{y\} = \{y\})$
43	9 42	ax-mp	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} x = \{y\} \leftrightarrow \{y\} = \{y\}$
44	43	3anbi2i	$⊢ (\neg A \in Fin \land \underset{˙}{[} \{y\} / x \underset{˙}{]} x = \{y\} \land \underset{˙}{[} \{y\} / x \underset{˙}{]} y \in A) \leftrightarrow (\neg A \in Fin \land \{y\} = \{y\} \land \underset{˙}{[} \{y\} / x \underset{˙}{]} y \in A)$
45	38 41 44	3bitri	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} (\neg A \in Fin \land x = \{y\} \land y \in A) \leftrightarrow (\neg A \in Fin \land \{y\} = \{y\} \land \underset{˙}{[} \{y\} / x \underset{˙}{]} y \in A)$
46		sbcg	$⊢ \{y\} \in V \to (\underset{˙}{[} \{y\} / x \underset{˙}{]} y \in A \leftrightarrow y \in A)$
47	9 46	ax-mp	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} y \in A \leftrightarrow y \in A$
48	47	3anbi3i	$⊢ (\neg A \in Fin \land \{y\} = \{y\} \land \underset{˙}{[} \{y\} / x \underset{˙}{]} y \in A) \leftrightarrow (\neg A \in Fin \land \{y\} = \{y\} \land y \in A)$
49	45 48	bitri	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} (\neg A \in Fin \land x = \{y\} \land y \in A) \leftrightarrow (\neg A \in Fin \land \{y\} = \{y\} \land y \in A)$
50		sbcg	$⊢ \{y\} \in V \to (\underset{˙}{[} \{y\} / x \underset{˙}{]} \{y\} \in T \leftrightarrow \{y\} \in T)$
51	9 50	ax-mp	$⊢ \underset{˙}{[} \{y\} / x \underset{˙}{]} \{y\} \in T \leftrightarrow \{y\} \in T$
52	37 49 51	3imtr3i	$⊢ (\neg A \in Fin \land \{y\} = \{y\} \land y \in A) \to \{y\} \in T$
53	8 52	mp3an2	$⊢ (\neg A \in Fin \land y \in A) \to \{y\} \in T$
54	53	ex	$⊢ \neg A \in Fin \to (y \in A \to \{y\} \in T)$
55	54	pm4.71d	$⊢ \neg A \in Fin \to (y \in A \leftrightarrow (y \in A \land \{y\} \in T))$
56	55	anbi1d	$⊢ \neg A \in Fin \to ((y \in A \land u = \{y\}) \leftrightarrow ((y \in A \land \{y\} \in T) \land u = \{y\}))$
57	56	exbidv	$⊢ \neg A \in Fin \to (\exists y (y \in A \land u = \{y\}) \leftrightarrow \exists y ((y \in A \land \{y\} \in T) \land u = \{y\}))$
58	7 57	syl5bb	$⊢ \neg A \in Fin \to (u \in \{u \| \exists y \in A u = \{y\}\} \leftrightarrow \exists y ((y \in A \land \{y\} \in T) \land u = \{y\}))$
59		anass	$⊢ ((y \in A \land \{y\} \in T) \land u = \{y\}) \leftrightarrow (y \in A \land (\{y\} \in T \land u = \{y\}))$
60	59	exbii	$⊢ \exists y ((y \in A \land \{y\} \in T) \land u = \{y\}) \leftrightarrow \exists y (y \in A \land (\{y\} \in T \land u = \{y\}))$
61		exsimpr	$⊢ \exists y (y \in A \land (\{y\} \in T \land u = \{y\})) \to \exists y (\{y\} \in T \land u = \{y\})$
62	60 61	sylbi	$⊢ \exists y ((y \in A \land \{y\} \in T) \land u = \{y\}) \to \exists y (\{y\} \in T \land u = \{y\})$
63	58 62	syl6bi	$⊢ \neg A \in Fin \to (u \in \{u \| \exists y \in A u = \{y\}\} \to \exists y (\{y\} \in T \land u = \{y\}))$
64		ancom	$⊢ (\{y\} \in T \land u = \{y\}) \leftrightarrow (u = \{y\} \land \{y\} \in T)$
65		eleq1	$⊢ u = \{y\} \to (u \in T \leftrightarrow \{y\} \in T)$
66	65	pm5.32i	$⊢ (u = \{y\} \land u \in T) \leftrightarrow (u = \{y\} \land \{y\} \in T)$
67	64 66	bitr4i	$⊢ (\{y\} \in T \land u = \{y\}) \leftrightarrow (u = \{y\} \land u \in T)$
68	67	exbii	$⊢ \exists y (\{y\} \in T \land u = \{y\}) \leftrightarrow \exists y (u = \{y\} \land u \in T)$
69	63 68	syl6ib	$⊢ \neg A \in Fin \to (u \in \{u \| \exists y \in A u = \{y\}\} \to \exists y (u = \{y\} \land u \in T))$
70		exsimpr	$⊢ \exists y (u = \{y\} \land u \in T) \to \exists y u \in T$
71	69 70	syl6	$⊢ \neg A \in Fin \to (u \in \{u \| \exists y \in A u = \{y\}\} \to \exists y u \in T)$
72		ax5e	$⊢ \exists y u \in T \to u \in T$
73	71 72	syl6	$⊢ \neg A \in Fin \to (u \in \{u \| \exists y \in A u = \{y\}\} \to u \in T)$
74	2 3 4 73	ssrd	$⊢ \neg A \in Fin \to \{u \| \exists y \in A u = \{y\}\} \subseteq T$
75		eqid	$⊢ \{u \| \exists y \in A u = \{y\}\} = \{u \| \exists y \in A u = \{y\}\}$
76	75	dissneq	$⊢ (\{u \| \exists y \in A u = \{y\}\} \subseteq T \land T \in TopOn (A)) \to T = 𝒫 A$
77	74 76	sylan	$⊢ (\neg A \in Fin \land T \in TopOn (A)) \to T = 𝒫 A$
78		nfielex	$⊢ \neg A \in Fin \to \exists y y \in A$
79	78	adantr	$⊢ (\neg A \in Fin \land T \in TopOn (A)) \to \exists y y \in A$
80		difss	$⊢ A ∖ \{y\} \subseteq A$
81		elfvex	$⊢ T \in TopOn (A) \to A \in V$
82		difexg	$⊢ A \in V \to A ∖ \{y\} \in V$
83		elpwg	$⊢ A ∖ \{y\} \in V \to (A ∖ \{y\} \in 𝒫 A \leftrightarrow A ∖ \{y\} \subseteq A)$
84	81 82 83	3syl	$⊢ T \in TopOn (A) \to (A ∖ \{y\} \in 𝒫 A \leftrightarrow A ∖ \{y\} \subseteq A)$
85	80 84	mpbiri	$⊢ T \in TopOn (A) \to A ∖ \{y\} \in 𝒫 A$
86	85	adantl	$⊢ (\neg A \in Fin \land T \in TopOn (A)) \to A ∖ \{y\} \in 𝒫 A$
87		difinf	$⊢ (\neg A \in Fin \land \{y\} \in Fin) \to \neg A ∖ \{y\} \in Fin$
88	18 87	mpan2	$⊢ \neg A \in Fin \to \neg A ∖ \{y\} \in Fin$
89		0fin	$⊢ \emptyset \in Fin$
90		eleq1	$⊢ A ∖ \{y\} = \emptyset \to (A ∖ \{y\} \in Fin \leftrightarrow \emptyset \in Fin)$
91	89 90	mpbiri	$⊢ A ∖ \{y\} = \emptyset \to A ∖ \{y\} \in Fin$
92	88 91	nsyl	$⊢ \neg A \in Fin \to \neg A ∖ \{y\} = \emptyset$
93	92	ad2antrl	$⊢ (y \in A \land (\neg A \in Fin \land T \in TopOn (A))) \to \neg A ∖ \{y\} = \emptyset$
94		vsnid	$⊢ y \in \{y\}$
95		inelcm	$⊢ (y \in A \land y \in \{y\}) \to A \cap \{y\} \neq \emptyset$
96	94 95	mpan2	$⊢ y \in A \to A \cap \{y\} \neq \emptyset$
97		disj4	$⊢ A \cap \{y\} = \emptyset \leftrightarrow \neg A ∖ \{y\} \subset A$
98	97	necon2abii	$⊢ A ∖ \{y\} \subset A \leftrightarrow A \cap \{y\} \neq \emptyset$
99	96 98	sylibr	$⊢ y \in A \to A ∖ \{y\} \subset A$
100	99	pssned	$⊢ y \in A \to A ∖ \{y\} \neq A$
101	100	adantr	$⊢ (y \in A \land (\neg A \in Fin \land T \in TopOn (A))) \to A ∖ \{y\} \neq A$
102	101	neneqd	$⊢ (y \in A \land (\neg A \in Fin \land T \in TopOn (A))) \to \neg A ∖ \{y\} = A$
103	93 102	jca	$⊢ (y \in A \land (\neg A \in Fin \land T \in TopOn (A))) \to (\neg A ∖ \{y\} = \emptyset \land \neg A ∖ \{y\} = A)$
104		pm4.56	$⊢ (\neg A ∖ \{y\} = \emptyset \land \neg A ∖ \{y\} = A) \leftrightarrow \neg (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A)$
105	103 104	sylib	$⊢ (y \in A \land (\neg A \in Fin \land T \in TopOn (A))) \to \neg (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A)$
106		difeq2	$⊢ x = A ∖ \{y\} \to A ∖ x = A ∖ (A ∖ \{y\})$
107	106	eleq1d	$⊢ x = A ∖ \{y\} \to (A ∖ x \in Fin \leftrightarrow A ∖ (A ∖ \{y\}) \in Fin)$
108	107	notbid	$⊢ x = A ∖ \{y\} \to (\neg A ∖ x \in Fin \leftrightarrow \neg A ∖ (A ∖ \{y\}) \in Fin)$
109		eqeq1	$⊢ x = A ∖ \{y\} \to (x = \emptyset \leftrightarrow A ∖ \{y\} = \emptyset)$
110		eqeq1	$⊢ x = A ∖ \{y\} \to (x = A \leftrightarrow A ∖ \{y\} = A)$
111	109 110	orbi12d	$⊢ x = A ∖ \{y\} \to ((x = \emptyset \lor x = A) \leftrightarrow (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A))$
112	108 111	orbi12d	$⊢ x = A ∖ \{y\} \to ((\neg A ∖ x \in Fin \lor (x = \emptyset \lor x = A)) \leftrightarrow (\neg A ∖ (A ∖ \{y\}) \in Fin \lor (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A)))$
113	112 1	elrab2	$⊢ A ∖ \{y\} \in T \leftrightarrow (A ∖ \{y\} \in 𝒫 A \land (\neg A ∖ (A ∖ \{y\}) \in Fin \lor (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A)))$
114	85	biantrurd	$⊢ T \in TopOn (A) \to ((\neg A ∖ (A ∖ \{y\}) \in Fin \lor (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A)) \leftrightarrow (A ∖ \{y\} \in 𝒫 A \land (\neg A ∖ (A ∖ \{y\}) \in Fin \lor (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A))))$
115	113 114	bitr4id	$⊢ T \in TopOn (A) \to (A ∖ \{y\} \in T \leftrightarrow (\neg A ∖ (A ∖ \{y\}) \in Fin \lor (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A)))$
116		dfin4	$⊢ A \cap \{y\} = A ∖ (A ∖ \{y\})$
117		inss2	$⊢ A \cap \{y\} \subseteq \{y\}$
118		ssfi	$⊢ (\{y\} \in Fin \land A \cap \{y\} \subseteq \{y\}) \to A \cap \{y\} \in Fin$
119	18 117 118	mp2an	$⊢ A \cap \{y\} \in Fin$
120	116 119	eqeltrri	$⊢ A ∖ (A ∖ \{y\}) \in Fin$
121		biortn	$⊢ A ∖ (A ∖ \{y\}) \in Fin \to ((A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A) \leftrightarrow (\neg A ∖ (A ∖ \{y\}) \in Fin \lor (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A)))$
122	120 121	ax-mp	$⊢ (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A) \leftrightarrow (\neg A ∖ (A ∖ \{y\}) \in Fin \lor (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A))$
123	115 122	bitr4di	$⊢ T \in TopOn (A) \to (A ∖ \{y\} \in T \leftrightarrow (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A))$
124	123	ad2antll	$⊢ (y \in A \land (\neg A \in Fin \land T \in TopOn (A))) \to (A ∖ \{y\} \in T \leftrightarrow (A ∖ \{y\} = \emptyset \lor A ∖ \{y\} = A))$
125	105 124	mtbird	$⊢ (y \in A \land (\neg A \in Fin \land T \in TopOn (A))) \to \neg A ∖ \{y\} \in T$
126	125	expcom	$⊢ (\neg A \in Fin \land T \in TopOn (A)) \to (y \in A \to \neg A ∖ \{y\} \in T)$
127		nelneq2	$⊢ (A ∖ \{y\} \in 𝒫 A \land \neg A ∖ \{y\} \in T) \to \neg 𝒫 A = T$
128		eqcom	$⊢ T = 𝒫 A \leftrightarrow 𝒫 A = T$
129	127 128	sylnibr	$⊢ (A ∖ \{y\} \in 𝒫 A \land \neg A ∖ \{y\} \in T) \to \neg T = 𝒫 A$
130	86 126 129	syl6an	$⊢ (\neg A \in Fin \land T \in TopOn (A)) \to (y \in A \to \neg T = 𝒫 A)$
131	79 130	exellimddv	$⊢ (\neg A \in Fin \land T \in TopOn (A)) \to \neg T = 𝒫 A$
132	77 131	pm2.65da	$⊢ \neg A \in Fin \to \neg T \in TopOn (A)$
133	132	con4i	$⊢ T \in TopOn (A) \to A \in Fin$

Metamath Proof Explorer

Theorem topdifinffinlem

Proof