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 10006

Description: Lemma for hsmex 10011. Bound the order type of a union of sets of ordinals, each of limited order type. Vaguely reminiscent of unictb 10154 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 4508	. . . . . 6 ⊢ (𝐵 ∈ 𝒫 On → 𝐵 ⊆ On)
2	1	adantr 484	. . . . 5 ⊢ ((𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → 𝐵 ⊆ On)
3	2	ralimi 3073	. . . 4 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
4		iunss 4940	. . . 4 ⊢ (∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ↔ ∀𝑎 ∈ 𝐴 𝐵 ⊆ On)
5	3, 4	sylibr 237	. . 3 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
6	5	3ad2ant3 1137	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On)
7		xpexg 7513	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On) → (𝐴 × 𝐶) ∈ V)
8	7	3adant3 1134	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐴 × 𝐶) ∈ V)
9		nfv 1922	. . . . . . . . 9 ⊢ Ⅎ𝑎 𝐶 ∈ On
10		nfra1 3130	. . . . . . . . 9 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)
11	9, 10	nfan 1907	. . . . . . . 8 ⊢ Ⅎ𝑎(𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶))
12		rsp 3117	. . . . . . . . 9 ⊢ (∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → (𝑎 ∈ 𝐴 → (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)))
13		onelss 6233	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ On → (dom 𝐹 ∈ 𝐶 → dom 𝐹 ⊆ 𝐶))
14	13	imp 410	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ On ∧ dom 𝐹 ∈ 𝐶) → dom 𝐹 ⊆ 𝐶)
15	14	adantrl 716	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → dom 𝐹 ⊆ 𝐶)
16	15	3adant3 1134	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) ∧ 𝑏 ∈ 𝐵) → dom 𝐹 ⊆ 𝐶)
17		hsmexlem.f	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = OrdIso( E , 𝐵)
18	17	oismo 9134	. . . . . . . . . . . . . . . . . 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 499	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ran 𝐹 = 𝐵)
22	17	oif 9124	. . . . . . . . . . . . . . 15 ⊢ 𝐹:dom 𝐹⟶𝐵
23	21, 22	jctil 523	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
24		dffo2 6615	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ran 𝐹 = 𝐵))
25	23, 24	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → 𝐹:dom 𝐹–onto→𝐵)
26		dffo3 6899	. . . . . . . . . . . . . 14 ⊢ (𝐹:dom 𝐹–onto→𝐵 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
27	26	simprbi 500	. . . . . . . . . . . . 13 ⊢ (𝐹:dom 𝐹–onto→𝐵 → ∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒))
28		rsp 3117	. . . . . . . . . . . . 13 ⊢ (∀𝑏 ∈ 𝐵 ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒) → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
29	25, 27, 28	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒)))
30	29	3impia 1119	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) ∧ 𝑏 ∈ 𝐵) → ∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒))
31		ssrexv 3954	. . . . . . . . . . 11 ⊢ (dom 𝐹 ⊆ 𝐶 → (∃𝑒 ∈ dom 𝐹 𝑏 = (𝐹‘𝑒) → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
32	16, 30, 31	sylc 65	. . . . . . . . . 10 ⊢ ((𝐶 ∈ On ∧ (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) ∧ 𝑏 ∈ 𝐵) → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒))
33	32	3exp 1121	. . . . . . . . 9 ⊢ (𝐶 ∈ On → ((𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶) → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒))))
34	12, 33	sylan9r 512	. . . . . . . 8 ⊢ ((𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝑎 ∈ 𝐴 → (𝑏 ∈ 𝐵 → ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒))))
35	11, 34	reximdai 3220	. . . . . . 7 ⊢ ((𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
36	35	3adant1 1132	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)))
37		nfv 1922	. . . . . . 7 ⊢ Ⅎ𝑑∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒)
38		nfcv 2897	. . . . . . . 8 ⊢ Ⅎ𝑎𝐶
39		nfcv 2897	. . . . . . . . . . 11 ⊢ Ⅎ𝑎 E
40		nfcsb1v 3823	. . . . . . . . . . 11 ⊢ Ⅎ𝑎⦋𝑑 / 𝑎⦌𝐵
41	39, 40	nfoi 9108	. . . . . . . . . 10 ⊢ Ⅎ𝑎OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)
42		nfcv 2897	. . . . . . . . . 10 ⊢ Ⅎ𝑎𝑒
43	41, 42	nffv 6705	. . . . . . . . 9 ⊢ Ⅎ𝑎(OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
44	43	nfeq2 2914	. . . . . . . 8 ⊢ Ⅎ𝑎 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
45	38, 44	nfrex 3218	. . . . . . 7 ⊢ Ⅎ𝑎∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)
46		csbeq1a 3812	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → 𝐵 = ⦋𝑑 / 𝑎⦌𝐵)
47		oieq2 9107	. . . . . . . . . . . 12 ⊢ (𝐵 = ⦋𝑑 / 𝑎⦌𝐵 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → OrdIso( E , 𝐵) = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
49	17, 48	syl5eq 2783	. . . . . . . . . 10 ⊢ (𝑎 = 𝑑 → 𝐹 = OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵))
50	49	fveq1d 6697	. . . . . . . . 9 ⊢ (𝑎 = 𝑑 → (𝐹‘𝑒) = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
51	50	eqeq2d 2747	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝑏 = (𝐹‘𝑒) ↔ 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
52	51	rexbidv 3206	. . . . . . 7 ⊢ (𝑎 = 𝑑 → (∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
53	37, 45, 52	cbvrexw 3340	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (𝐹‘𝑒) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
54	36, 53	syl6ib 254	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
55		eliun 4894	. . . . 5 ⊢ (𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 ↔ ∃𝑎 ∈ 𝐴 𝑏 ∈ 𝐵)
56		vex 3402	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
57		vex 3402	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
58	56, 57	op1std 7749	. . . . . . . . . 10 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (1^st ‘𝑐) = 𝑑)
59	58	csbeq1d 3802	. . . . . . . . 9 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → ⦋(1^st ‘𝑐) / 𝑎⦌𝐵 = ⦋𝑑 / 𝑎⦌𝐵)
60		oieq2 9107	. . . . . . . . 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 7750	. . . . . . . 8 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (2^nd ‘𝑐) = 𝑒)
63	61, 62	fveq12d 6702	. . . . . . 7 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
64	63	eqeq2d 2747	. . . . . 6 ⊢ (𝑐 = ⟨𝑑, 𝑒⟩ → (𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) ↔ 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒)))
65	64	rexxp 5696	. . . . 5 ⊢ (∃𝑐 ∈ (𝐴 × 𝐶)𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐶 𝑏 = (OrdIso( E , ⦋𝑑 / 𝑎⦌𝐵)‘𝑒))
66	54, 55, 65	3imtr4g 299	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → (𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 → ∃𝑐 ∈ (𝐴 × 𝐶)𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐))))
67	66	imp 410	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) ∧ 𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵) → ∃𝑐 ∈ (𝐴 × 𝐶)𝑏 = (OrdIso( E , ⦋(1^st ‘𝑐) / 𝑎⦌𝐵)‘(2^nd ‘𝑐)))
68	8, 67	wdomd 9175	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → ∪ 𝑎 ∈ 𝐴 𝐵 ≼^* (𝐴 × 𝐶))
69		hsmexlem.g	. . 3 ⊢ 𝐺 = OrdIso( E , ∪ 𝑎 ∈ 𝐴 𝐵)
70	69	hsmexlem1 10005	. 2 ⊢ ((∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ∧ ∪ 𝑎 ∈ 𝐴 𝐵 ≼^* (𝐴 × 𝐶)) → dom 𝐺 ∈ (har‘𝒫 (𝐴 × 𝐶)))
71	6, 68, 70	syl2anc 587	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → dom 𝐺 ∈ (har‘𝒫 (𝐴 × 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2112 ∀wral 3051 ∃wrex 3052 Vcvv 3398 ⦋csb 3798 ⊆ wss 3853 𝒫 cpw 4499 ⟨cop 4533 ∪ ciun 4890 class class class wbr 5039 E cep 5444 × cxp 5534 dom cdm 5536 ran crn 5537 Oncon0 6191 ⟶wf 6354 –onto→wfo 6356 ‘cfv 6358 1^st c1st 7737 2^nd c2nd 7738 Smo wsmo 8060 OrdIsocoi 9103 harchar 9150 ≼^* cwdom 9158

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3400 df-sbc 3684 df-csb 3799 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-tp 4532 df-op 4534 df-uni 4806 df-iun 4892 df-br 5040 df-opab 5102 df-mpt 5121 df-tr 5147 df-id 5440 df-eprel 5445 df-po 5453 df-so 5454 df-fr 5494 df-se 5495 df-we 5496 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-pred 6140 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6316 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-isom 6367 df-riota 7148 df-1st 7739 df-2nd 7740 df-wrecs 8025 df-smo 8061 df-recs 8086 df-er 8369 df-en 8605 df-dom 8606 df-sdom 8607 df-oi 9104 df-har 9151 df-wdom 9159

This theorem is referenced by: hsmexlem3 10007

W3C validator