fin1a2lem12

		Ref	Expression
	Assertion	fin1a2lem12	$⊢ ((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \to \neg B \in {Fin}^{III}$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to B \in {Fin}^{III}$
2		simpll1	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to A \subseteq 𝒫 B$
3	2	adantr	$⊢ ((((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \land e \in ω) \to A \subseteq 𝒫 B$
4		ssrab2	$⊢ \{f \in A \| f ≼ e\} \subseteq A$
5	4	unissi	$⊢ ⋃ \{f \in A \| f ≼ e\} \subseteq ⋃ A$
6		sspwuni	$⊢ A \subseteq 𝒫 B \leftrightarrow ⋃ A \subseteq B$
7	6	biimpi	$⊢ A \subseteq 𝒫 B \to ⋃ A \subseteq B$
8	5 7	sstrid	$⊢ A \subseteq 𝒫 B \to ⋃ \{f \in A \| f ≼ e\} \subseteq B$
9	3 8	syl	$⊢ ((((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \land e \in ω) \to ⋃ \{f \in A \| f ≼ e\} \subseteq B$
10		elpw2g	$⊢ B \in {Fin}^{III} \to (⋃ \{f \in A \| f ≼ e\} \in 𝒫 B \leftrightarrow ⋃ \{f \in A \| f ≼ e\} \subseteq B)$
11	10	ad2antlr	$⊢ ((((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \land e \in ω) \to (⋃ \{f \in A \| f ≼ e\} \in 𝒫 B \leftrightarrow ⋃ \{f \in A \| f ≼ e\} \subseteq B)$
12	9 11	mpbird	$⊢ ((((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \land e \in ω) \to ⋃ \{f \in A \| f ≼ e\} \in 𝒫 B$
13	12	fmpttd	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) : ω ⟶ 𝒫 B$
14		vex	$⊢ d \in V$
15	14	sucex	$⊢ suc d \in V$
16		sssucid	$⊢ d \subseteq suc d$
17		ssdomg	$⊢ suc d \in V \to (d \subseteq suc d \to d ≼ suc d)$
18	15 16 17	mp2	$⊢ d ≼ suc d$
19		domtr	$⊢ (f ≼ d \land d ≼ suc d) \to f ≼ suc d$
20	18 19	mpan2	$⊢ f ≼ d \to f ≼ suc d$
21	20	a1i	$⊢ f \in A \to (f ≼ d \to f ≼ suc d)$
22	21	ss2rabi	$⊢ \{f \in A \| f ≼ d\} \subseteq \{f \in A \| f ≼ suc d\}$
23		uniss	$⊢ \{f \in A \| f ≼ d\} \subseteq \{f \in A \| f ≼ suc d\} \to ⋃ \{f \in A \| f ≼ d\} \subseteq ⋃ \{f \in A \| f ≼ suc d\}$
24	22 23	mp1i	$⊢ ((((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \land d \in ω) \to ⋃ \{f \in A \| f ≼ d\} \subseteq ⋃ \{f \in A \| f ≼ suc d\}$
25		id	$⊢ d \in ω \to d \in ω$
26		pwexg	$⊢ B \in {Fin}^{III} \to 𝒫 B \in V$
27	26	adantl	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to 𝒫 B \in V$
28	27 2	ssexd	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to A \in V$
29		rabexg	$⊢ A \in V \to \{f \in A \| f ≼ d\} \in V$
30		uniexg	$⊢ \{f \in A \| f ≼ d\} \in V \to ⋃ \{f \in A \| f ≼ d\} \in V$
31	28 29 30	3syl	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to ⋃ \{f \in A \| f ≼ d\} \in V$
32		breq2	$⊢ e = d \to (f ≼ e \leftrightarrow f ≼ d)$
33	32	rabbidv	$⊢ e = d \to \{f \in A \| f ≼ e\} = \{f \in A \| f ≼ d\}$
34	33	unieqd	$⊢ e = d \to ⋃ \{f \in A \| f ≼ e\} = ⋃ \{f \in A \| f ≼ d\}$
35		eqid	$⊢ (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\})$
36	34 35	fvmptg	$⊢ (d \in ω \land ⋃ \{f \in A \| f ≼ d\} \in V) \to (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (d) = ⋃ \{f \in A \| f ≼ d\}$
37	25 31 36	syl2anr	$⊢ ((((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \land d \in ω) \to (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (d) = ⋃ \{f \in A \| f ≼ d\}$
38		peano2	$⊢ d \in ω \to suc d \in ω$
39		rabexg	$⊢ A \in V \to \{f \in A \| f ≼ suc d\} \in V$
40		uniexg	$⊢ \{f \in A \| f ≼ suc d\} \in V \to ⋃ \{f \in A \| f ≼ suc d\} \in V$
41	28 39 40	3syl	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to ⋃ \{f \in A \| f ≼ suc d\} \in V$
42		breq2	$⊢ e = suc d \to (f ≼ e \leftrightarrow f ≼ suc d)$
43	42	rabbidv	$⊢ e = suc d \to \{f \in A \| f ≼ e\} = \{f \in A \| f ≼ suc d\}$
44	43	unieqd	$⊢ e = suc d \to ⋃ \{f \in A \| f ≼ e\} = ⋃ \{f \in A \| f ≼ suc d\}$
45	44 35	fvmptg	$⊢ (suc d \in ω \land ⋃ \{f \in A \| f ≼ suc d\} \in V) \to (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (suc d) = ⋃ \{f \in A \| f ≼ suc d\}$
46	38 41 45	syl2anr	$⊢ ((((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \land d \in ω) \to (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (suc d) = ⋃ \{f \in A \| f ≼ suc d\}$
47	24 37 46	3sstr4d	$⊢ ((((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \land d \in ω) \to (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (d) \subseteq (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (suc d)$
48	47	ralrimiva	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to \forall d \in ω (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (d) \subseteq (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (suc d)$
49		fin34i	$⊢ (B \in {Fin}^{III} \land (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) : ω ⟶ 𝒫 B \land \forall d \in ω (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (d) \subseteq (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) (suc d)) \to ⋃ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) \in ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\})$
50	1 13 48 49	syl3anc	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to ⋃ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) \in ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\})$
51		fin1a2lem11	$⊢ ([\subset] Or A \land A \subseteq Fin) \to ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\}$
52	51	adantrr	$⊢ ([\subset] Or A \land (A \subseteq Fin \land A \neq \emptyset)) \to ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\}$
53	52	3ad2antl2	$⊢ ((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \to ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\}$
54	53	adantr	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\}$
55		simpll3	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to \neg ⋃ A \in A$
56		simplrr	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to A \neq \emptyset$
57		sspwuni	$⊢ A \subseteq 𝒫 \emptyset \leftrightarrow ⋃ A \subseteq \emptyset$
58		ss0b	$⊢ ⋃ A \subseteq \emptyset \leftrightarrow ⋃ A = \emptyset$
59	57 58	bitri	$⊢ A \subseteq 𝒫 \emptyset \leftrightarrow ⋃ A = \emptyset$
60		pw0	$⊢ 𝒫 \emptyset = \{\emptyset\}$
61	60	sseq2i	$⊢ A \subseteq 𝒫 \emptyset \leftrightarrow A \subseteq \{\emptyset\}$
62		sssn	$⊢ A \subseteq \{\emptyset\} \leftrightarrow (A = \emptyset \lor A = \{\emptyset\})$
63	61 62	bitri	$⊢ A \subseteq 𝒫 \emptyset \leftrightarrow (A = \emptyset \lor A = \{\emptyset\})$
64		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
65		0ex	$⊢ \emptyset \in V$
66	65	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
67	65	snid	$⊢ \emptyset \in \{\emptyset\}$
68	66 67	eqeltri	$⊢ ⋃ \{\emptyset\} \in \{\emptyset\}$
69		unieq	$⊢ A = \{\emptyset\} \to ⋃ A = ⋃ \{\emptyset\}$
70		id	$⊢ A = \{\emptyset\} \to A = \{\emptyset\}$
71	69 70	eleq12d	$⊢ A = \{\emptyset\} \to (⋃ A \in A \leftrightarrow ⋃ \{\emptyset\} \in \{\emptyset\})$
72	68 71	mpbiri	$⊢ A = \{\emptyset\} \to ⋃ A \in A$
73	72	orim2i	$⊢ (A = \emptyset \lor A = \{\emptyset\}) \to (A = \emptyset \lor ⋃ A \in A)$
74	73	ord	$⊢ (A = \emptyset \lor A = \{\emptyset\}) \to (\neg A = \emptyset \to ⋃ A \in A)$
75	64 74	syl5bi	$⊢ (A = \emptyset \lor A = \{\emptyset\}) \to (A \neq \emptyset \to ⋃ A \in A)$
76	63 75	sylbi	$⊢ A \subseteq 𝒫 \emptyset \to (A \neq \emptyset \to ⋃ A \in A)$
77	59 76	sylbir	$⊢ ⋃ A = \emptyset \to (A \neq \emptyset \to ⋃ A \in A)$
78	77	com12	$⊢ A \neq \emptyset \to (⋃ A = \emptyset \to ⋃ A \in A)$
79	78	con3d	$⊢ A \neq \emptyset \to (\neg ⋃ A \in A \to \neg ⋃ A = \emptyset)$
80	56 55 79	sylc	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to \neg ⋃ A = \emptyset$
81		ioran	$⊢ \neg (⋃ A \in A \lor ⋃ A = \emptyset) \leftrightarrow (\neg ⋃ A \in A \land \neg ⋃ A = \emptyset)$
82	55 80 81	sylanbrc	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to \neg (⋃ A \in A \lor ⋃ A = \emptyset)$
83		uniun	$⊢ ⋃ (A \cup \{\emptyset\}) = ⋃ A \cup ⋃ \{\emptyset\}$
84	66	uneq2i	$⊢ ⋃ A \cup ⋃ \{\emptyset\} = ⋃ A \cup \emptyset$
85		un0	$⊢ ⋃ A \cup \emptyset = ⋃ A$
86	83 84 85	3eqtri	$⊢ ⋃ (A \cup \{\emptyset\}) = ⋃ A$
87	86	eleq1i	$⊢ ⋃ (A \cup \{\emptyset\}) \in (A \cup \{\emptyset\}) \leftrightarrow ⋃ A \in (A \cup \{\emptyset\})$
88		elun	$⊢ ⋃ A \in (A \cup \{\emptyset\}) \leftrightarrow (⋃ A \in A \lor ⋃ A \in \{\emptyset\})$
89	65	elsn2	$⊢ ⋃ A \in \{\emptyset\} \leftrightarrow ⋃ A = \emptyset$
90	89	orbi2i	$⊢ (⋃ A \in A \lor ⋃ A \in \{\emptyset\}) \leftrightarrow (⋃ A \in A \lor ⋃ A = \emptyset)$
91	87 88 90	3bitri	$⊢ ⋃ (A \cup \{\emptyset\}) \in (A \cup \{\emptyset\}) \leftrightarrow (⋃ A \in A \lor ⋃ A = \emptyset)$
92	82 91	sylnibr	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to \neg ⋃ (A \cup \{\emptyset\}) \in (A \cup \{\emptyset\})$
93		unieq	$⊢ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\} \to ⋃ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = ⋃ (A \cup \{\emptyset\})$
94		id	$⊢ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\} \to ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\}$
95	93 94	eleq12d	$⊢ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\} \to (⋃ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) \in ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) \leftrightarrow ⋃ (A \cup \{\emptyset\}) \in (A \cup \{\emptyset\}))$
96	95	notbid	$⊢ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\} \to (\neg ⋃ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) \in ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) \leftrightarrow \neg ⋃ (A \cup \{\emptyset\}) \in (A \cup \{\emptyset\}))$
97	92 96	syl5ibrcom	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to (ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) = A \cup \{\emptyset\} \to \neg ⋃ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) \in ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}))$
98	54 97	mpd	$⊢ (((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \land B \in {Fin}^{III}) \to \neg ⋃ ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\}) \in ran (e \in ω ⟼ ⋃ \{f \in A \| f ≼ e\})$
99	50 98	pm2.65da	$⊢ ((A \subseteq 𝒫 B \land [\subset] Or A \land \neg ⋃ A \in A) \land (A \subseteq Fin \land A \neq \emptyset)) \to \neg B \in {Fin}^{III}$

Metamath Proof Explorer

Theorem fin1a2lem12

Proof