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 4587	. . . . . 6 ⊢ (𝐵 ∈ 𝒫 On → 𝐵 ⊆ On)
2	1	adantr 481	. . . . 5 ⊢ ((𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → 𝐵 ⊆ On)
3	2	ralimi 3082	. . . 4 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
4		iunss 5025	. . . 4 ⊢ (∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ↔ ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
5	3, 4	sylibr 233	. . 3 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
6	5	3ad2ant3 1135	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
7		xpexg 7704	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On) → (𝐴 × 𝐶) ∈ V)
8	7	3adant3 1132	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐴 × 𝐶) ∈ V)
9		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑎 𝐶 ∈ On
10		nfra1 3278	. . . . . . . . 9 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)
11	9, 10	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑎(𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶))
12		rsp 3241	. . . . . . . . 9 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → (𝑎 ∈ 𝐴 → (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)))
13		onelss 6379	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ On → (dom 𝐹 ∈ 𝐶 → dom 𝐹 ⊆ 𝐶))
14	13	imp 407	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ On ∧ dom 𝐹 ∈ 𝐶) → dom 𝐹 ⊆ 𝐶)
15	14	adantrl 714	. . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (Smo 𝐹 ∧ ran 𝐹 = 𝐵))
21	20	simprd 496	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ran 𝐹 = 𝐵)
22	17	oif 9490	. . . . . . . . . . . . . . 15 ⊢ 𝐹:dom 𝐹⟶𝐵
23	21, 22	jctil 520	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
24		dffo2 6780	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
25	23, 24	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → 𝐹:dom 𝐹–onto→𝐵)
26		dffo3 7072	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
27	26	simprbi 497	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐵 → ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒))
28		rsp 3241	. . . . . . . . . . . . 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 4031	. . . . . . . . . . 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 509	. . . . . . . 8 ⊢ ((𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝑎 ∈ 𝐴 → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒))))
35	11, 34	reximdai 3255	. . . . . . 7 ⊢ ((𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
36	35	3adant1 1130	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
37		nfv 1917	. . . . . . 7 ⊢ Ⅎ𝑑∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)
38		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑎𝐶
39		nfcv 2902	. . . . . . . . . . 11 ⊢ Ⅎ𝑎 E
40		nfcsb1v 3898	. . . . . . . . . . 11 ⊢ Ⅎ𝑎⦋𝑑 / 𝑎⦌𝐵
41	39, 40	nfoi 9474	. . . . . . . . . 10 ⊢ Ⅎ𝑎OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)
42		nfcv 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑎𝑒
43	41, 42	nffv 6872	. . . . . . . . 9 ⊢ Ⅎ𝑎(OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
44	43	nfeq2 2919	. . . . . . . 8 ⊢ Ⅎ𝑎 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
45	38, 44	nfrexw 3307	. . . . . . 7 ⊢ Ⅎ𝑎∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
46		csbeq1a 3887	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → 𝐵 = ⦋𝑑 / 𝑎⦌𝐵)
47		oieq2 9473	. . . . . . . . . . . 12 ⊢ (𝐵 = ⦋𝑑 / 𝑎⦌𝐵 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
49	17, 48	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → 𝐹 = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
50	49	fveq1d 6864	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (𝐹‘𝑒) = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
51	50	eqeq2d 2742	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝑏 = (𝐹‘𝑒) ↔ 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
52	51	rexbidv 3177	. . . . . . 7 ⊢ (𝑎 = 𝑑 → (∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
53	37, 45, 52	cbvrexw 3301	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
54	36, 53	syl6ib 250	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
55		eliun 4978	. . . . 5 ⊢ (𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 ↔ ∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵)
56		vex 3463	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
57		vex 3463	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
58	56, 57	op1std 7951	. . . . . . . . . 10 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (1^st ‘𝑐) = 𝑑)
59	58	csbeq1d 3877	. . . . . . . . 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 7952	. . . . . . . 8 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (2^nd ‘𝑐) = 𝑒)
63	61, 62	fveq12d 6869	. . . . . . 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 5818	. . . . 5 ⊢ (∃𝑐 ∈ (𝐴 × 𝐶)𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
66	54, 55, 65	3imtr4g 295	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 → ∃𝑐 ∈ (𝐴 × 𝐶)𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐))))
67	66	imp 407	. . 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 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3060 ∃wrex 3069 Vcvv 3459 ⦋csb 3873 ⊆ wss 3928 𝒫 cpw 4580 ⟨cop 4612 ∪ ciun 4974 class class class wbr 5125 E cep 5556 × cxp 5651 dom cdm 5653 ran crn 5654 Oncon0 6337 ⟶wf 6512 –onto→wfo 6514 ‘cfv 6516 1^st c1st 7939 2^nd c2nd 7940 Smo wsmo 8311 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 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5262 ax-sep 5276 ax-nul 5283 ax-pow 5340 ax-pr 5404 ax-un 7692

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3364 df-reu 3365 df-rab 3419 df-v 3461 df-sbc 3758 df-csb 3874 df-dif 3931 df-un 3933 df-in 3935 df-ss 3945 df-pss 3947 df-nul 4303 df-if 4507 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4886 df-iun 4976 df-br 5126 df-opab 5188 df-mpt 5209 df-tr 5243 df-id 5551 df-eprel 5557 df-po 5565 df-so 5566 df-fr 5608 df-se 5609 df-we 5610 df-xp 5659 df-rel 5660 df-cnv 5661 df-co 5662 df-dm 5663 df-rn 5664 df-res 5665 df-ima 5666 df-pred 6273 df-ord 6340 df-on 6341 df-lim 6342 df-suc 6343 df-iota 6468 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7333 df-ov 7380 df-1st 7941 df-2nd 7942 df-frecs 8232 df-wrecs 8263 df-smo 8312 df-recs 8337 df-en 8906 df-dom 8907 df-sdom 8908 df-oi 9470 df-har 9517 df-wdom 9525

This theorem is referenced by: hsmexlem3 10388

W3C validator