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 10318

Description: Lemma for hsmex 10323. Bound the order type of a union of sets of ordinals, each of limited order type. Vaguely reminiscent of unictb 10466 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 4554	. . . . . 6 ⊢ (𝐵 ∈ 𝒫 On → 𝐵 ⊆ On)
2	1	adantr 480	. . . . 5 ⊢ ((𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → 𝐵 ⊆ On)
3	2	ralimi 3069	. . . 4 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
4		iunss 4992	. . . 4 ⊢ (∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ↔ ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
5	3, 4	sylibr 234	. . 3 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
6	5	3ad2ant3 1135	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
7		xpexg 7683	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On) → (𝐴 × 𝐶) ∈ V)
8	7	3adant3 1132	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐴 × 𝐶) ∈ V)
9		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑎 𝐶 ∈ On
10		nfra1 3256	. . . . . . . . 9 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)
11	9, 10	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑎(𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶))
12		rsp 3220	. . . . . . . . 9 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → (𝑎 ∈ 𝐴 → (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)))
13		onelss 6348	. . . . . . . . . . . . . 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 9426	. . . . . . . . . . . . . . . . . 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 9416	. . . . . . . . . . . . . . 15 ⊢ 𝐹:dom 𝐹⟶𝐵
23	21, 22	jctil 519	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
24		dffo2 6739	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
25	23, 24	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → 𝐹:dom 𝐹–onto→𝐵)
26		dffo3 7035	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
27	26	simprbi 496	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐵 → ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒))
28		rsp 3220	. . . . . . . . . . . . 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 3999	. . . . . . . . . . 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 3234	. . . . . . 7 ⊢ ((𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
36	35	3adant1 1130	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
37		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑑∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)
38		nfcv 2894	. . . . . . . 8 ⊢ Ⅎ𝑎𝐶
39		nfcv 2894	. . . . . . . . . . 11 ⊢ Ⅎ𝑎 E
40		nfcsb1v 3869	. . . . . . . . . . 11 ⊢ Ⅎ𝑎⦋𝑑 / 𝑎⦌𝐵
41	39, 40	nfoi 9400	. . . . . . . . . 10 ⊢ Ⅎ𝑎OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)
42		nfcv 2894	. . . . . . . . . 10 ⊢ Ⅎ𝑎𝑒
43	41, 42	nffv 6832	. . . . . . . . 9 ⊢ Ⅎ𝑎(OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
44	43	nfeq2 2912	. . . . . . . 8 ⊢ Ⅎ𝑎 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
45	38, 44	nfrexw 3280	. . . . . . 7 ⊢ Ⅎ𝑎∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
46		csbeq1a 3859	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → 𝐵 = ⦋𝑑 / 𝑎⦌𝐵)
47		oieq2 9399	. . . . . . . . . . . 12 ⊢ (𝐵 = ⦋𝑑 / 𝑎⦌𝐵 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
49	17, 48	eqtrid 2778	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → 𝐹 = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
50	49	fveq1d 6824	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (𝐹‘𝑒) = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
51	50	eqeq2d 2742	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝑏 = (𝐹‘𝑒) ↔ 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
52	51	rexbidv 3156	. . . . . . 7 ⊢ (𝑎 = 𝑑 → (∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
53	37, 45, 52	cbvrexw 3275	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
54	36, 53	imbitrdi 251	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
55		eliun 4943	. . . . 5 ⊢ (𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 ↔ ∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵)
56		vex 3440	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
57		vex 3440	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
58	56, 57	op1std 7931	. . . . . . . . . 10 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (1^st ‘𝑐) = 𝑑)
59	58	csbeq1d 3849	. . . . . . . . 9 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → ⦋(1^st ‘𝑐) / 𝑎⦌𝐵 = ⦋𝑑 / 𝑎⦌𝐵)
60		oieq2 9399	. . . . . . . . 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 7932	. . . . . . . 8 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (2^nd ‘𝑐) = 𝑒)
63	61, 62	fveq12d 6829	. . . . . . 7 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
64	63	eqeq2d 2742	. . . . . 6 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) ↔ 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
65	64	rexxp 5781	. . . . 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 9467	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ∪ 𝑎 ∈ 𝐴 𝐵 ≼^* (𝐴 × 𝐶))
69		hsmexlem.g	. . 3 ⊢ 𝐺 = OrdIso( E , ∪ 𝑎 ∈ 𝐴 𝐵)
70	69	hsmexlem1 10317	. 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 1541 ∈ wcel 2111 ∀wral 3047 ∃wrex 3056 Vcvv 3436 ⦋csb 3845 ⊆ wss 3897 𝒫 cpw 4547 ⟨cop 4579 ∪ ciun 4939 class class class wbr 5089 E cep 5513 × cxp 5612 dom cdm 5614 ran crn 5615 Oncon0 6306 ⟶wf 6477 –onto→wfo 6479 ‘cfv 6481 1^st c1st 7919 2^nd c2nd 7920 Smo wsmo 8265 OrdIsocoi 9395 harchar 9442 ≼^* cwdom 9450

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-smo 8266 df-recs 8291 df-en 8870 df-dom 8871 df-sdom 8872 df-oi 9396 df-har 9443 df-wdom 9451

This theorem is referenced by: hsmexlem3 10319

W3C validator