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 10387

Description: Lemma for hsmex 10392. Bound the order type of a union of sets of ordinals, each of limited order type. Vaguely reminiscent of unictb 10535 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 4573	. . . . . 6 ⊢ (𝐵 ∈ 𝒫 On → 𝐵 ⊆ On)
2	1	adantr 480	. . . . 5 ⊢ ((𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → 𝐵 ⊆ On)
3	2	ralimi 3067	. . . 4 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
4		iunss 5012	. . . 4 ⊢ (∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ↔ ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
5	3, 4	sylibr 234	. . 3 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
6	5	3ad2ant3 1135	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
7		xpexg 7729	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On) → (𝐴 × 𝐶) ∈ V)
8	7	3adant3 1132	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐴 × 𝐶) ∈ V)
9		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑎 𝐶 ∈ On
10		nfra1 3262	. . . . . . . . 9 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)
11	9, 10	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑎(𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶))
12		rsp 3226	. . . . . . . . 9 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → (𝑎 ∈ 𝐴 → (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)))
13		onelss 6377	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ On → (dom 𝐹 ∈ 𝐶 → dom 𝐹 ⊆ 𝐶))
14	13	imp 406	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ On ∧ dom 𝐹 ∈ 𝐶) → dom 𝐹 ⊆ 𝐶)
15	14	adantrl 716	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → dom 𝐹 ⊆ 𝐶)
16	15	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) ∧ 𝑏 ∈ 𝐵) → dom 𝐹 ⊆ 𝐶)
17		hsmexlem.f	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = OrdIso( E , 𝐵)
18	17	oismo 9500	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐵))
19	1, 18	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ 𝒫 On → (Smo 𝐹 ∧ ran 𝐹 = 𝐵))
20	19	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (Smo 𝐹 ∧ ran 𝐹 = 𝐵))
21	20	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ran 𝐹 = 𝐵)
22	17	oif 9490	. . . . . . . . . . . . . . 15 ⊢ 𝐹:dom 𝐹⟶𝐵
23	21, 22	jctil 519	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
24		dffo2 6779	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
25	23, 24	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → 𝐹:dom 𝐹–onto→𝐵)
26		dffo3 7077	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
27	26	simprbi 496	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐵 → ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒))
28		rsp 3226	. . . . . . . . . . . . 13 ⊢ (∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒) → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
29	25, 27, 28	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
30	29	3impia 1117	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) ∧ 𝑏 ∈ 𝐵) → ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒))
31		ssrexv 4019	. . . . . . . . . . 11 ⊢ (dom 𝐹 ⊆ 𝐶 → (∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒) → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
32	16, 30, 31	sylc 65	. . . . . . . . . 10 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) ∧ 𝑏 ∈ 𝐵) → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒))
33	32	3exp 1119	. . . . . . . . 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 1130	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
37		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑑∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)
38		nfcv 2892	. . . . . . . 8 ⊢ Ⅎ𝑎𝐶
39		nfcv 2892	. . . . . . . . . . 11 ⊢ Ⅎ𝑎 E
40		nfcsb1v 3889	. . . . . . . . . . 11 ⊢ Ⅎ𝑎⦋𝑑 / 𝑎⦌𝐵
41	39, 40	nfoi 9474	. . . . . . . . . 10 ⊢ Ⅎ𝑎OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)
42		nfcv 2892	. . . . . . . . . 10 ⊢ Ⅎ𝑎𝑒
43	41, 42	nffv 6871	. . . . . . . . 9 ⊢ Ⅎ𝑎(OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
44	43	nfeq2 2910	. . . . . . . 8 ⊢ Ⅎ𝑎 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
45	38, 44	nfrexw 3289	. . . . . . 7 ⊢ Ⅎ𝑎∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
46		csbeq1a 3879	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → 𝐵 = ⦋𝑑 / 𝑎⦌𝐵)
47		oieq2 9473	. . . . . . . . . . . 12 ⊢ (𝐵 = ⦋𝑑 / 𝑎⦌𝐵 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
49	17, 48	eqtrid 2777	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → 𝐹 = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
50	49	fveq1d 6863	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (𝐹‘𝑒) = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
51	50	eqeq2d 2741	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝑏 = (𝐹‘𝑒) ↔ 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
52	51	rexbidv 3158	. . . . . . 7 ⊢ (𝑎 = 𝑑 → (∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
53	37, 45, 52	cbvrexw 3283	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
54	36, 53	imbitrdi 251	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
55		eliun 4962	. . . . 5 ⊢ (𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 ↔ ∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵)
56		vex 3454	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
57		vex 3454	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
58	56, 57	op1std 7981	. . . . . . . . . 10 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (1^st ‘𝑐) = 𝑑)
59	58	csbeq1d 3869	. . . . . . . . 9 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → ⦋(1^st ‘𝑐) / 𝑎⦌𝐵 = ⦋𝑑 / 𝑎⦌𝐵)
60		oieq2 9473	. . . . . . . . 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 7982	. . . . . . . 8 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (2^nd ‘𝑐) = 𝑒)
63	61, 62	fveq12d 6868	. . . . . . 7 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
64	63	eqeq2d 2741	. . . . . 6 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) ↔ 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
65	64	rexxp 5809	. . . . 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 9541	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ∪ 𝑎 ∈ 𝐴 𝐵 ≼^* (𝐴 × 𝐶))
69		hsmexlem.g	. . 3 ⊢ 𝐺 = OrdIso( E , ∪ 𝑎 ∈ 𝐴 𝐵)
70	69	hsmexlem1 10386	. 2 ⊢ ((∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ∧ ∪ 𝑎 ∈ 𝐴 𝐵 ≼^* (𝐴 × 𝐶)) → dom 𝐺 ∈ (har‘𝒫 (𝐴 × 𝐶)))
71	6, 68, 70	syl2anc 584	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → dom 𝐺 ∈ (har‘𝒫 (𝐴 × 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3045 ∃wrex 3054 Vcvv 3450 ⦋csb 3865 ⊆ wss 3917 𝒫 cpw 4566 ⟨cop 4598 ∪ ciun 4958 class class class wbr 5110 E cep 5540 × cxp 5639 dom cdm 5641 ran crn 5642 Oncon0 6335 ⟶wf 6510 –onto→wfo 6512 ‘cfv 6514 1^st c1st 7969 2^nd c2nd 7970 Smo wsmo 8317 OrdIsocoi 9469 harchar 9516 ≼^* cwdom 9524

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-smo 8318 df-recs 8343 df-en 8922 df-dom 8923 df-sdom 8924 df-oi 9470 df-har 9517 df-wdom 9525

This theorem is referenced by: hsmexlem3 10388

W3C validator