hsmexlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hsmexlem2		Structured version Visualization version GIF version

Theorem hsmexlem2 10349

Description: Lemma for hsmex 10354. Bound the order type of a union of sets of ordinals, each of limited order type. Vaguely reminiscent of unictb 10498 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.)

**Hypotheses**
Ref	Expression
hsmexlem.f	⊢ 𝐹 = OrdIso( E , 𝐵)
hsmexlem.g	⊢ 𝐺 = OrdIso( E , ∪ 𝑎 ∈ 𝐴 𝐵)

**Assertion**
Ref	Expression
hsmexlem2	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → dom 𝐺 ∈ (har‘𝒫 (𝐴 × 𝐶)))

Distinct variable groups: 𝐴,𝑎 𝐶,𝑎 Allowed substitution hints: 𝐵(𝑎) 𝐹(𝑎) 𝐺(𝑎) 𝑉(𝑎)

Proof of Theorem hsmexlem2 Dummy variables 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpwi 4563	. . . . . 6 ⊢ (𝐵 ∈ 𝒫 On → 𝐵 ⊆ On)
2	1	adantr 480	. . . . 5 ⊢ ((𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → 𝐵 ⊆ On)
3	2	ralimi 3075	. . . 4 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
4		iunss 5002	. . . 4 ⊢ (∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ↔ ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
5	3, 4	sylibr 234	. . 3 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
6	5	3ad2ant3 1136	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
7		xpexg 7705	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On) → (𝐴 × 𝐶) ∈ V)
8	7	3adant3 1133	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐴 × 𝐶) ∈ V)
9		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑎 𝐶 ∈ On
10		nfra1 3262	. . . . . . . . 9 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)
11	9, 10	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑎(𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶))
12		rsp 3226	. . . . . . . . 9 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → (𝑎 ∈ 𝐴 → (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)))
13		onelss 6367	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ On → (dom 𝐹 ∈ 𝐶 → dom 𝐹 ⊆ 𝐶))
14	13	imp 406	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ On ∧ dom 𝐹 ∈ 𝐶) → dom 𝐹 ⊆ 𝐶)
15	14	adantrl 717	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → dom 𝐹 ⊆ 𝐶)
16	15	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) ∧ 𝑏 ∈ 𝐵) → dom 𝐹 ⊆ 𝐶)
17		hsmexlem.f	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = OrdIso( E , 𝐵)
18	17	oismo 9457	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐵))
19	1, 18	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ 𝒫 On → (Smo 𝐹 ∧ ran 𝐹 = 𝐵))
20	19	ad2antrl 729	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (Smo 𝐹 ∧ ran 𝐹 = 𝐵))
21	20	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ran 𝐹 = 𝐵)
22	17	oif 9447	. . . . . . . . . . . . . . 15 ⊢ 𝐹:dom 𝐹⟶𝐵
23	21, 22	jctil 519	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
24		dffo2 6758	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
25	23, 24	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → 𝐹:dom 𝐹–onto→𝐵)
26		dffo3 7056	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
27	26	simprbi 497	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐵 → ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒))
28		rsp 3226	. . . . . . . . . . . . 13 ⊢ (∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒) → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
29	25, 27, 28	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
30	29	3impia 1118	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) ∧ 𝑏 ∈ 𝐵) → ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒))
31		ssrexv 4005	. . . . . . . . . . 11 ⊢ (dom 𝐹 ⊆ 𝐶 → (∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒) → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
32	16, 30, 31	sylc 65	. . . . . . . . . 10 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) ∧ 𝑏 ∈ 𝐵) → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒))
33	32	3exp 1120	. . . . . . . . 9 ⊢ (𝐶 ∈ On → ((𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒))))
34	12, 33	sylan9r 508	. . . . . . . 8 ⊢ ((𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝑎 ∈ 𝐴 → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒))))
35	11, 34	reximdai 3240	. . . . . . 7 ⊢ ((𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
36	35	3adant1 1131	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
37		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑑∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)
38		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑎𝐶
39		nfcv 2899	. . . . . . . . . . 11 ⊢ Ⅎ𝑎 E
40		nfcsb1v 3875	. . . . . . . . . . 11 ⊢ Ⅎ𝑎⦋𝑑 / 𝑎⦌𝐵
41	39, 40	nfoi 9431	. . . . . . . . . 10 ⊢ Ⅎ𝑎OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)
42		nfcv 2899	. . . . . . . . . 10 ⊢ Ⅎ𝑎𝑒
43	41, 42	nffv 6852	. . . . . . . . 9 ⊢ Ⅎ𝑎(OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
44	43	nfeq2 2917	. . . . . . . 8 ⊢ Ⅎ𝑎 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
45	38, 44	nfrexw 3286	. . . . . . 7 ⊢ Ⅎ𝑎∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
46		csbeq1a 3865	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → 𝐵 = ⦋𝑑 / 𝑎⦌𝐵)
47		oieq2 9430	. . . . . . . . . . . 12 ⊢ (𝐵 = ⦋𝑑 / 𝑎⦌𝐵 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
49	17, 48	eqtrid 2784	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → 𝐹 = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
50	49	fveq1d 6844	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (𝐹‘𝑒) = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
51	50	eqeq2d 2748	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝑏 = (𝐹‘𝑒) ↔ 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
52	51	rexbidv 3162	. . . . . . 7 ⊢ (𝑎 = 𝑑 → (∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
53	37, 45, 52	cbvrexw 3281	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
54	36, 53	imbitrdi 251	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
55		eliun 4952	. . . . 5 ⊢ (𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 ↔ ∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵)
56		vex 3446	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
57		vex 3446	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
58	56, 57	op1std 7953	. . . . . . . . . 10 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (1^st ‘𝑐) = 𝑑)
59	58	csbeq1d 3855	. . . . . . . . 9 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → ⦋(1^st ‘𝑐) / 𝑎⦌𝐵 = ⦋𝑑 / 𝑎⦌𝐵)
60		oieq2 9430	. . . . . . . . 9 ⊢ (⦋(1^st ‘𝑐) / 𝑎⦌𝐵 = ⦋𝑑 / 𝑎⦌𝐵 → OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
61	59, 60	syl 17	. . . . . . . 8 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
62	56, 57	op2ndd 7954	. . . . . . . 8 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (2^nd ‘𝑐) = 𝑒)
63	61, 62	fveq12d 6849	. . . . . . 7 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
64	63	eqeq2d 2748	. . . . . 6 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) ↔ 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
65	64	rexxp 5799	. . . . 5 ⊢ (∃𝑐 ∈ (𝐴 × 𝐶)𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
66	54, 55, 65	3imtr4g 296	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 → ∃𝑐 ∈ (𝐴 × 𝐶)𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐))))
67	66	imp 406	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) ∧ 𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵) → ∃𝑐 ∈ (𝐴 × 𝐶)𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)))
68	8, 67	wdomd 9498	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ∪ 𝑎 ∈ 𝐴 𝐵 ≼^* (𝐴 × 𝐶))
69		hsmexlem.g	. . 3 ⊢ 𝐺 = OrdIso( E , ∪ 𝑎 ∈ 𝐴 𝐵)
70	69	hsmexlem1 10348	. 2 ⊢ ((∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ∧ ∪ 𝑎 ∈ 𝐴 𝐵 ≼^* (𝐴 × 𝐶)) → dom 𝐺 ∈ (har‘𝒫 (𝐴 × 𝐶)))
71	6, 68, 70	syl2anc 585	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → dom 𝐺 ∈ (har‘𝒫 (𝐴 × 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 Vcvv 3442 ⦋csb 3851 ⊆ wss 3903 𝒫 cpw 4556 ⟨cop 4588 ∪ ciun 4948 class class class wbr 5100 E cep 5531 × cxp 5630 dom cdm 5632 ran crn 5633 Oncon0 6325 ⟶wf 6496 –onto→wfo 6498 ‘cfv 6500 1^st c1st 7941 2^nd c2nd 7942 Smo wsmo 8287 OrdIsocoi 9426 harchar 9473 ≼^* cwdom 9481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-smo 8288 df-recs 8313 df-en 8896 df-dom 8897 df-sdom 8898 df-oi 9427 df-har 9474 df-wdom 9482

This theorem is referenced by: hsmexlem3 10350

W3C validator