hsmexlem2

Description: Lemma for hsmex . Bound the order type of a union of sets of ordinals, each of limited order type. Vaguely reminiscent of unictb but use of order types allows to canonically choose the sub-bijections, removing the choice requirement. (Contributed by Stefan O'Rear, 14-Feb-2015) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 18-Sep-2021)

	Ref	Expression
Hypotheses	hsmexlem.f	$⊢ F = OrdIso (E, B)$
	hsmexlem.g	$⊢ G = OrdIso (E, ⋃_{a \in A} B)$
Assertion	hsmexlem2	$⊢ (A \in V \land C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to dom G \in har (𝒫 (A \times C))$

Proof

Step	Hyp	Ref	Expression
1		hsmexlem.f	$⊢ F = OrdIso (E, B)$
2		hsmexlem.g	$⊢ G = OrdIso (E, ⋃_{a \in A} B)$
3		elpwi	$⊢ B \in 𝒫 On \to B \subseteq On$
4	3	adantr	$⊢ (B \in 𝒫 On \land dom F \in C) \to B \subseteq On$
5	4	ralimi	$⊢ \forall a \in A (B \in 𝒫 On \land dom F \in C) \to \forall a \in A B \subseteq On$
6		iunss	$⊢ ⋃_{a \in A} B \subseteq On \leftrightarrow \forall a \in A B \subseteq On$
7	5 6	sylibr	$⊢ \forall a \in A (B \in 𝒫 On \land dom F \in C) \to ⋃_{a \in A} B \subseteq On$
8	7	3ad2ant3	$⊢ (A \in V \land C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to ⋃_{a \in A} B \subseteq On$
9		xpexg	$⊢ (A \in V \land C \in On) \to A \times C \in V$
10	9	3adant3	$⊢ (A \in V \land C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to A \times C \in V$
11		nfv	$⊢ Ⅎ a C \in On$
12		nfra1	$⊢ Ⅎ a \forall a \in A (B \in 𝒫 On \land dom F \in C)$
13	11 12	nfan	$⊢ Ⅎ a (C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C))$
14		rsp	$⊢ \forall a \in A (B \in 𝒫 On \land dom F \in C) \to (a \in A \to (B \in 𝒫 On \land dom F \in C))$
15		onelss	$⊢ C \in On \to (dom F \in C \to dom F \subseteq C)$
16	15	imp	$⊢ (C \in On \land dom F \in C) \to dom F \subseteq C$
17	16	adantrl	$⊢ (C \in On \land (B \in 𝒫 On \land dom F \in C)) \to dom F \subseteq C$
18	17	3adant3	$⊢ (C \in On \land (B \in 𝒫 On \land dom F \in C) \land b \in B) \to dom F \subseteq C$
19	1	oismo	$⊢ B \subseteq On \to (Smo F \land ran F = B)$
20	3 19	syl	$⊢ B \in 𝒫 On \to (Smo F \land ran F = B)$
21	20	ad2antrl	$⊢ (C \in On \land (B \in 𝒫 On \land dom F \in C)) \to (Smo F \land ran F = B)$
22	21	simprd	$⊢ (C \in On \land (B \in 𝒫 On \land dom F \in C)) \to ran F = B$
23	1	oif	$⊢ F : dom F ⟶ B$
24	22 23	jctil	$⊢ (C \in On \land (B \in 𝒫 On \land dom F \in C)) \to (F : dom F ⟶ B \land ran F = B)$
25		dffo2	$⊢ F : dom F \underset{onto}{⟶} B \leftrightarrow (F : dom F ⟶ B \land ran F = B)$
26	24 25	sylibr	$⊢ (C \in On \land (B \in 𝒫 On \land dom F \in C)) \to F : dom F \underset{onto}{⟶} B$
27		dffo3	$⊢ F : dom F \underset{onto}{⟶} B \leftrightarrow (F : dom F ⟶ B \land \forall b \in B \exists e \in dom F b = F (e))$
28	27	simprbi	$⊢ F : dom F \underset{onto}{⟶} B \to \forall b \in B \exists e \in dom F b = F (e)$
29		rsp	$⊢ \forall b \in B \exists e \in dom F b = F (e) \to (b \in B \to \exists e \in dom F b = F (e))$
30	26 28 29	3syl	$⊢ (C \in On \land (B \in 𝒫 On \land dom F \in C)) \to (b \in B \to \exists e \in dom F b = F (e))$
31	30	3impia	$⊢ (C \in On \land (B \in 𝒫 On \land dom F \in C) \land b \in B) \to \exists e \in dom F b = F (e)$
32		ssrexv	$⊢ dom F \subseteq C \to (\exists e \in dom F b = F (e) \to \exists e \in C b = F (e))$
33	18 31 32	sylc	$⊢ (C \in On \land (B \in 𝒫 On \land dom F \in C) \land b \in B) \to \exists e \in C b = F (e)$
34	33	3exp	$⊢ C \in On \to ((B \in 𝒫 On \land dom F \in C) \to (b \in B \to \exists e \in C b = F (e)))$
35	14 34	sylan9r	$⊢ (C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to (a \in A \to (b \in B \to \exists e \in C b = F (e)))$
36	13 35	reximdai	$⊢ (C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to (\exists a \in A b \in B \to \exists a \in A \exists e \in C b = F (e))$
37	36	3adant1	$⊢ (A \in V \land C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to (\exists a \in A b \in B \to \exists a \in A \exists e \in C b = F (e))$
38		nfv	$⊢ Ⅎ d \exists e \in C b = F (e)$
39		nfcv	$⊢ \underline{Ⅎ} a C$
40		nfcv	$⊢ \underline{Ⅎ} a E$
41		nfcsb1v	$⊢ \underline{Ⅎ} a ⦋ d / a ⦌ B$
42	40 41	nfoi	$⊢ \underline{Ⅎ} a OrdIso (E, ⦋ d / a ⦌ B)$
43		nfcv	$⊢ \underline{Ⅎ} a e$
44	42 43	nffv	$⊢ \underline{Ⅎ} a OrdIso (E, ⦋ d / a ⦌ B) (e)$
45	44	nfeq2	$⊢ Ⅎ a b = OrdIso (E, ⦋ d / a ⦌ B) (e)$
46	39 45	nfrexw	$⊢ Ⅎ a \exists e \in C b = OrdIso (E, ⦋ d / a ⦌ B) (e)$
47		csbeq1a	$⊢ a = d \to B = ⦋ d / a ⦌ B$
48		oieq2	$⊢ B = ⦋ d / a ⦌ B \to OrdIso (E, B) = OrdIso (E, ⦋ d / a ⦌ B)$
49	47 48	syl	$⊢ a = d \to OrdIso (E, B) = OrdIso (E, ⦋ d / a ⦌ B)$
50	1 49	eqtrid	$⊢ a = d \to F = OrdIso (E, ⦋ d / a ⦌ B)$
51	50	fveq1d	$⊢ a = d \to F (e) = OrdIso (E, ⦋ d / a ⦌ B) (e)$
52	51	eqeq2d	$⊢ a = d \to (b = F (e) \leftrightarrow b = OrdIso (E, ⦋ d / a ⦌ B) (e))$
53	52	rexbidv	$⊢ a = d \to (\exists e \in C b = F (e) \leftrightarrow \exists e \in C b = OrdIso (E, ⦋ d / a ⦌ B) (e))$
54	38 46 53	cbvrexw	$⊢ \exists a \in A \exists e \in C b = F (e) \leftrightarrow \exists d \in A \exists e \in C b = OrdIso (E, ⦋ d / a ⦌ B) (e)$
55	37 54	imbitrdi	$⊢ (A \in V \land C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to (\exists a \in A b \in B \to \exists d \in A \exists e \in C b = OrdIso (E, ⦋ d / a ⦌ B) (e))$
56		eliun	$⊢ b \in ⋃_{a \in A} B \leftrightarrow \exists a \in A b \in B$
57		vex	$⊢ d \in V$
58		vex	$⊢ e \in V$
59	57 58	op1std	$⊢ c = ⟨d, e⟩ \to 1^{st} (c) = d$
60	59	csbeq1d	$⊢ c = ⟨d, e⟩ \to ⦋ 1^{st} (c) / a ⦌ B = ⦋ d / a ⦌ B$
61		oieq2	$⊢ ⦋ 1^{st} (c) / a ⦌ B = ⦋ d / a ⦌ B \to OrdIso (E, ⦋ 1^{st} (c) / a ⦌ B) = OrdIso (E, ⦋ d / a ⦌ B)$
62	60 61	syl	$⊢ c = ⟨d, e⟩ \to OrdIso (E, ⦋ 1^{st} (c) / a ⦌ B) = OrdIso (E, ⦋ d / a ⦌ B)$
63	57 58	op2ndd	$⊢ c = ⟨d, e⟩ \to 2^{nd} (c) = e$
64	62 63	fveq12d	$⊢ c = ⟨d, e⟩ \to OrdIso (E, ⦋ 1^{st} (c) / a ⦌ B) (2^{nd} (c)) = OrdIso (E, ⦋ d / a ⦌ B) (e)$
65	64	eqeq2d	$⊢ c = ⟨d, e⟩ \to (b = OrdIso (E, ⦋ 1^{st} (c) / a ⦌ B) (2^{nd} (c)) \leftrightarrow b = OrdIso (E, ⦋ d / a ⦌ B) (e))$
66	65	rexxp	$⊢ \exists c \in (A \times C) b = OrdIso (E, ⦋ 1^{st} (c) / a ⦌ B) (2^{nd} (c)) \leftrightarrow \exists d \in A \exists e \in C b = OrdIso (E, ⦋ d / a ⦌ B) (e)$
67	55 56 66	3imtr4g	$⊢ (A \in V \land C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to (b \in ⋃_{a \in A} B \to \exists c \in (A \times C) b = OrdIso (E, ⦋ 1^{st} (c) / a ⦌ B) (2^{nd} (c)))$
68	67	imp	$⊢ ((A \in V \land C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \land b \in ⋃_{a \in A} B) \to \exists c \in (A \times C) b = OrdIso (E, ⦋ 1^{st} (c) / a ⦌ B) (2^{nd} (c))$
69	10 68	wdomd	$⊢ (A \in V \land C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to ⋃_{a \in A} B ≼^{*} (A \times C)$
70	2	hsmexlem1	$⊢ (⋃_{a \in A} B \subseteq On \land ⋃_{a \in A} B ≼^{*} (A \times C)) \to dom G \in har (𝒫 (A \times C))$
71	8 69 70	syl2anc	$⊢ (A \in V \land C \in On \land \forall a \in A (B \in 𝒫 On \land dom F \in C)) \to dom G \in har (𝒫 (A \times C))$

Metamath Proof Explorer

Theorem hsmexlem2

Proof