iunfictbso

Description: Countability of a countable union of finite sets with a strict (not globally well) order fulfilling the choice role. (Contributed by Stefan O'Rear, 16-Nov-2014)

		Ref	Expression
	Assertion	iunfictbso	$⊢ (A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \to ⋃ A ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		omex	$⊢ ω \in V$
2	1	0dom	$⊢ \emptyset ≼ ω$
3		breq1	$⊢ ⋃ A = \emptyset \to (⋃ A ≼ ω \leftrightarrow \emptyset ≼ ω)$
4	2 3	mpbiri	$⊢ ⋃ A = \emptyset \to ⋃ A ≼ ω$
5	4	a1d	$⊢ ⋃ A = \emptyset \to ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \to ⋃ A ≼ ω)$
6		n0	$⊢ ⋃ A \neq \emptyset \leftrightarrow \exists a a \in ⋃ A$
7		ne0i	$⊢ a \in ⋃ A \to ⋃ A \neq \emptyset$
8		unieq	$⊢ A = \emptyset \to ⋃ A = ⋃ \emptyset$
9		uni0	$⊢ ⋃ \emptyset = \emptyset$
10	8 9	eqtrdi	$⊢ A = \emptyset \to ⋃ A = \emptyset$
11	10	necon3i	$⊢ ⋃ A \neq \emptyset \to A \neq \emptyset$
12	7 11	syl	$⊢ a \in ⋃ A \to A \neq \emptyset$
13	12	adantl	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land a \in ⋃ A) \to A \neq \emptyset$
14		simpl1	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land a \in ⋃ A) \to A ≼ ω$
15		ctex	$⊢ A ≼ ω \to A \in V$
16		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
17	14 15 16	3syl	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land a \in ⋃ A) \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
18	13 17	mpbird	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land a \in ⋃ A) \to \emptyset ≺ A$
19		fodomr	$⊢ (\emptyset ≺ A \land A ≼ ω) \to \exists b b : ω \underset{onto}{⟶} A$
20	18 14 19	syl2anc	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land a \in ⋃ A) \to \exists b b : ω \underset{onto}{⟶} A$
21		omelon	$⊢ ω \in On$
22		onenon	$⊢ ω \in On \to ω \in dom card$
23	21 22	ax-mp	$⊢ ω \in dom card$
24		xpnum	$⊢ (ω \in dom card \land ω \in dom card) \to ω \times ω \in dom card$
25	23 23 24	mp2an	$⊢ ω \times ω \in dom card$
26		simplrr	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to b : ω \underset{onto}{⟶} A$
27		fof	$⊢ b : ω \underset{onto}{⟶} A \to b : ω ⟶ A$
28	26 27	syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to b : ω ⟶ A$
29		simprl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to f \in ω$
30	28 29	ffvelrnd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to b (f) \in A$
31	30	adantr	$⊢ ((((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \land g \in card (b (f))) \to b (f) \in A$
32		elssuni	$⊢ b (f) \in A \to b (f) \subseteq ⋃ A$
33	31 32	syl	$⊢ ((((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \land g \in card (b (f))) \to b (f) \subseteq ⋃ A$
34	30 32	syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to b (f) \subseteq ⋃ A$
35		simpll3	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to B Or ⋃ A$
36		soss	$⊢ b (f) \subseteq ⋃ A \to (B Or ⋃ A \to B Or b (f))$
37	34 35 36	sylc	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to B Or b (f)$
38		simpll2	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to A \subseteq Fin$
39	38 30	sseldd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to b (f) \in Fin$
40		finnisoeu	$⊢ (B Or b (f) \land b (f) \in Fin) \to \exists! h h {Isom}_{E, B} (card (b (f)), b (f))$
41	37 39 40	syl2anc	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to \exists! h h {Isom}_{E, B} (card (b (f)), b (f))$
42		iotacl	$⊢ \exists! h h {Isom}_{E, B} (card (b (f)), b (f)) \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) \in \{h \| h {Isom}_{E, B} (card (b (f)), b (f))\}$
43	41 42	syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) \in \{h \| h {Isom}_{E, B} (card (b (f)), b (f))\}$
44		iotaex	$⊢ (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) \in V$
45		isoeq1	$⊢ a = (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) \to (a {Isom}_{E, B} (card (b (f)), b (f)) \leftrightarrow (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) {Isom}_{E, B} (card (b (f)), b (f)))$
46		isoeq1	$⊢ h = a \to (h {Isom}_{E, B} (card (b (f)), b (f)) \leftrightarrow a {Isom}_{E, B} (card (b (f)), b (f)))$
47	46	cbvabv	$⊢ \{h \| h {Isom}_{E, B} (card (b (f)), b (f))\} = \{a \| a {Isom}_{E, B} (card (b (f)), b (f))\}$
48	44 45 47	elab2	$⊢ (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) \in \{h \| h {Isom}_{E, B} (card (b (f)), b (f))\} \leftrightarrow (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) {Isom}_{E, B} (card (b (f)), b (f))$
49	43 48	sylib	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) {Isom}_{E, B} (card (b (f)), b (f))$
50		isof1o	$⊢ (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) {Isom}_{E, B} (card (b (f)), b (f)) \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) : card (b (f)) \underset{1-1 onto}{⟶} b (f)$
51		f1of	$⊢ (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) : card (b (f)) \underset{1-1 onto}{⟶} b (f) \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) : card (b (f)) ⟶ b (f)$
52	49 50 51	3syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) : card (b (f)) ⟶ b (f)$
53	52	ffvelrnda	$⊢ ((((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \land g \in card (b (f))) \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g) \in b (f)$
54	33 53	sseldd	$⊢ ((((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \land g \in card (b (f))) \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g) \in ⋃ A$
55		simprl	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to a \in ⋃ A$
56	55	ad2antrr	$⊢ ((((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \land \neg g \in card (b (f))) \to a \in ⋃ A$
57	54 56	ifclda	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (f \in ω \land g \in ω)) \to if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a) \in ⋃ A$
58	57	ralrimivva	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to \forall f \in ω \forall g \in ω if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a) \in ⋃ A$
59		eqid	$⊢ (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) = (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a))$
60	59	fmpo	$⊢ \forall f \in ω \forall g \in ω if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a) \in ⋃ A \leftrightarrow (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) : ω \times ω ⟶ ⋃ A$
61	58 60	sylib	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) : ω \times ω ⟶ ⋃ A$
62		eluni	$⊢ c \in ⋃ A \leftrightarrow \exists i (c \in i \land i \in A)$
63		simplrr	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (c \in i \land i \in A)) \to b : ω \underset{onto}{⟶} A$
64		simprr	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (c \in i \land i \in A)) \to i \in A$
65		foelrn	$⊢ (b : ω \underset{onto}{⟶} A \land i \in A) \to \exists j \in ω i = b (j)$
66	63 64 65	syl2anc	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (c \in i \land i \in A)) \to \exists j \in ω i = b (j)$
67		simprrl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to j \in ω$
68		ordom	$⊢ Ord ω$
69		simpll2	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to A \subseteq Fin$
70		simplrr	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to b : ω \underset{onto}{⟶} A$
71	70 27	syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to b : ω ⟶ A$
72	71 67	ffvelrnd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to b (j) \in A$
73	69 72	sseldd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to b (j) \in Fin$
74		ficardom	$⊢ b (j) \in Fin \to card (b (j)) \in ω$
75	73 74	syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to card (b (j)) \in ω$
76		ordelss	$⊢ (Ord ω \land card (b (j)) \in ω) \to card (b (j)) \subseteq ω$
77	68 75 76	sylancr	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to card (b (j)) \subseteq ω$
78		elssuni	$⊢ b (j) \in A \to b (j) \subseteq ⋃ A$
79	72 78	syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to b (j) \subseteq ⋃ A$
80		simpll3	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to B Or ⋃ A$
81		soss	$⊢ b (j) \subseteq ⋃ A \to (B Or ⋃ A \to B Or b (j))$
82	79 80 81	sylc	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to B Or b (j)$
83		finnisoeu	$⊢ (B Or b (j) \land b (j) \in Fin) \to \exists! h h {Isom}_{E, B} (card (b (j)), b (j))$
84	82 73 83	syl2anc	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to \exists! h h {Isom}_{E, B} (card (b (j)), b (j))$
85		iotacl	$⊢ \exists! h h {Isom}_{E, B} (card (b (j)), b (j)) \to (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) \in \{h \| h {Isom}_{E, B} (card (b (j)), b (j))\}$
86	84 85	syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) \in \{h \| h {Isom}_{E, B} (card (b (j)), b (j))\}$
87		iotaex	$⊢ (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) \in V$
88		isoeq1	$⊢ a = (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) \to (a {Isom}_{E, B} (card (b (j)), b (j)) \leftrightarrow (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) {Isom}_{E, B} (card (b (j)), b (j)))$
89		isoeq1	$⊢ h = a \to (h {Isom}_{E, B} (card (b (j)), b (j)) \leftrightarrow a {Isom}_{E, B} (card (b (j)), b (j)))$
90	89	cbvabv	$⊢ \{h \| h {Isom}_{E, B} (card (b (j)), b (j))\} = \{a \| a {Isom}_{E, B} (card (b (j)), b (j))\}$
91	87 88 90	elab2	$⊢ (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) \in \{h \| h {Isom}_{E, B} (card (b (j)), b (j))\} \leftrightarrow (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) {Isom}_{E, B} (card (b (j)), b (j))$
92	86 91	sylib	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) {Isom}_{E, B} (card (b (j)), b (j))$
93		isof1o	$⊢ (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) {Isom}_{E, B} (card (b (j)), b (j)) \to (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) : card (b (j)) \underset{1-1 onto}{⟶} b (j)$
94	92 93	syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) : card (b (j)) \underset{1-1 onto}{⟶} b (j)$
95		f1ocnv	$⊢ (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) : card (b (j)) \underset{1-1 onto}{⟶} b (j) \to {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} : b (j) \underset{1-1 onto}{⟶} card (b (j))$
96		f1of	$⊢ {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} : b (j) \underset{1-1 onto}{⟶} card (b (j)) \to {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} : b (j) ⟶ card (b (j))$
97	94 95 96	3syl	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} : b (j) ⟶ card (b (j))$
98		simprll	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to c \in i$
99		simprrr	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to i = b (j)$
100	98 99	eleqtrd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to c \in b (j)$
101	97 100	ffvelrnd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in card (b (j))$
102	77 101	sseldd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in ω$
103		2fveq3	$⊢ f = j \to card (b (f)) = card (b (j))$
104	103	eleq2d	$⊢ f = j \to (g \in card (b (f)) \leftrightarrow g \in card (b (j)))$
105		isoeq4	$⊢ card (b (f)) = card (b (j)) \to (h {Isom}_{E, B} (card (b (f)), b (f)) \leftrightarrow h {Isom}_{E, B} (card (b (j)), b (f)))$
106	103 105	syl	$⊢ f = j \to (h {Isom}_{E, B} (card (b (f)), b (f)) \leftrightarrow h {Isom}_{E, B} (card (b (j)), b (f)))$
107		fveq2	$⊢ f = j \to b (f) = b (j)$
108		isoeq5	$⊢ b (f) = b (j) \to (h {Isom}_{E, B} (card (b (j)), b (f)) \leftrightarrow h {Isom}_{E, B} (card (b (j)), b (j)))$
109	107 108	syl	$⊢ f = j \to (h {Isom}_{E, B} (card (b (j)), b (f)) \leftrightarrow h {Isom}_{E, B} (card (b (j)), b (j)))$
110	106 109	bitrd	$⊢ f = j \to (h {Isom}_{E, B} (card (b (f)), b (f)) \leftrightarrow h {Isom}_{E, B} (card (b (j)), b (j)))$
111	110	iotabidv	$⊢ f = j \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) = (ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))$
112	111	fveq1d	$⊢ f = j \to (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g) = (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) (g)$
113	104 112	ifbieq1d	$⊢ f = j \to if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a) = if (g \in card (b (j)), (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) (g), a)$
114		eleq1	$⊢ g = {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \to (g \in card (b (j)) \leftrightarrow {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in card (b (j)))$
115		fveq2	$⊢ g = {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \to (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) (g) = (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c))$
116	114 115	ifbieq1d	$⊢ g = {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \to if (g \in card (b (j)), (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) (g), a) = if ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in card (b (j)), (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)), a)$
117		fvex	$⊢ (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)) \in V$
118		vex	$⊢ a \in V$
119	117 118	ifex	$⊢ if ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in card (b (j)), (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)), a) \in V$
120	113 116 59 119	ovmpo	$⊢ (j \in ω \land {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in ω) \to j (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) = if ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in card (b (j)), (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)), a)$
121	67 102 120	syl2anc	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to j (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) = if ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in card (b (j)), (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)), a)$
122	101	iftrued	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to if ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in card (b (j)), (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)), a) = (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c))$
123		f1ocnvfv2	$⊢ ((ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) : card (b (j)) \underset{1-1 onto}{⟶} b (j) \land c \in b (j)) \to (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)) = c$
124	94 100 123	syl2anc	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to (ι h \| h {Isom}_{E, B} (card (b (j)), b (j))) ({(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)) = c$
125	121 122 124	3eqtrrd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to c = j (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)$
126		rspceov	$⊢ (j \in ω \land {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c) \in ω \land c = j (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) {(ι h \| h {Isom}_{E, B} (card (b (j)), b (j)))}^{-1} (c)) \to \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e$
127	67 102 125 126	syl3anc	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land ((c \in i \land i \in A) \land (j \in ω \land i = b (j)))) \to \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e$
128	127	expr	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (c \in i \land i \in A)) \to ((j \in ω \land i = b (j)) \to \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e)$
129	128	expd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (c \in i \land i \in A)) \to (j \in ω \to (i = b (j) \to \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e))$
130	129	rexlimdv	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (c \in i \land i \in A)) \to (\exists j \in ω i = b (j) \to \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e)$
131	66 130	mpd	$⊢ (((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \land (c \in i \land i \in A)) \to \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e$
132	131	ex	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to ((c \in i \land i \in A) \to \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e)$
133	132	exlimdv	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to (\exists i (c \in i \land i \in A) \to \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e)$
134	62 133	syl5bi	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to (c \in ⋃ A \to \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e)$
135	134	ralrimiv	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to \forall c \in ⋃ A \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e$
136		foov	$⊢ (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) : ω \times ω \underset{onto}{⟶} ⋃ A \leftrightarrow ((f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) : ω \times ω ⟶ ⋃ A \land \forall c \in ⋃ A \exists d \in ω \exists e \in ω c = d (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) e)$
137	61 135 136	sylanbrc	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to (f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) : ω \times ω \underset{onto}{⟶} ⋃ A$
138		fodomnum	$⊢ ω \times ω \in dom card \to ((f \in ω, g \in ω ⟼ if (g \in card (b (f)), (ι h \| h {Isom}_{E, B} (card (b (f)), b (f))) (g), a)) : ω \times ω \underset{onto}{⟶} ⋃ A \to ⋃ A ≼ (ω \times ω))$
139	25 137 138	mpsyl	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to ⋃ A ≼ (ω \times ω)$
140		xpomen	$⊢ (ω \times ω) \approx ω$
141		domentr	$⊢ (⋃ A ≼ (ω \times ω) \land (ω \times ω) \approx ω) \to ⋃ A ≼ ω$
142	139 140 141	sylancl	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land (a \in ⋃ A \land b : ω \underset{onto}{⟶} A)) \to ⋃ A ≼ ω$
143	142	expr	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land a \in ⋃ A) \to (b : ω \underset{onto}{⟶} A \to ⋃ A ≼ ω)$
144	143	exlimdv	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land a \in ⋃ A) \to (\exists b b : ω \underset{onto}{⟶} A \to ⋃ A ≼ ω)$
145	20 144	mpd	$⊢ ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \land a \in ⋃ A) \to ⋃ A ≼ ω$
146	145	expcom	$⊢ a \in ⋃ A \to ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \to ⋃ A ≼ ω)$
147	146	exlimiv	$⊢ \exists a a \in ⋃ A \to ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \to ⋃ A ≼ ω)$
148	6 147	sylbi	$⊢ ⋃ A \neq \emptyset \to ((A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \to ⋃ A ≼ ω)$
149	5 148	pm2.61ine	$⊢ (A ≼ ω \land A \subseteq Fin \land B Or ⋃ A) \to ⋃ A ≼ ω$

Metamath Proof Explorer

Theorem iunfictbso

Proof