Theorem hsmexlem2

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

	Ref	Expression
Hypotheses	hsmexlem.f	⊢ 𝐹 = OrdIso ( E , 𝐵 )
	hsmexlem.g	⊢ 𝐺 = OrdIso ( E , ∪ 𝑎 ∈ 𝐴 𝐵 )
Assertion	hsmexlem2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hsmexlem.f	⊢ 𝐹 = OrdIso ( E , 𝐵 )
2		hsmexlem.g	⊢ 𝐺 = OrdIso ( E , ∪ 𝑎 ∈ 𝐴 𝐵 )
3		elpwi	⊢ ( 𝐵 ∈ 𝒫 On → 𝐵 ⊆ On )
4	3	adantr	⊢ ( ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) → 𝐵 ⊆ On )
5	4	ralimi	⊢ ( ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) → ∀ 𝑎 ∈ 𝐴 𝐵 ⊆ On )
6		iunss	⊢ ( ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ↔ ∀ 𝑎 ∈ 𝐴 𝐵 ⊆ On )
7	5 6	sylibr	⊢ ( ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On )
8	7	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On )
9		xpexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ) → ( 𝐴 × 𝐶 ) ∈ V )
10	9	3adant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( 𝐴 × 𝐶 ) ∈ V )
11		nfv	⊢ Ⅎ 𝑎 𝐶 ∈ On
12		nfra1	⊢ Ⅎ 𝑎 ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 )
13	11 12	nfan	⊢ Ⅎ 𝑎 ( 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) )
14		rsp	⊢ ( ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) → ( 𝑎 ∈ 𝐴 → ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) )
15		onelss	⊢ ( 𝐶 ∈ On → ( dom 𝐹 ∈ 𝐶 → dom 𝐹 ⊆ 𝐶 ) )
16	15	imp	⊢ ( ( 𝐶 ∈ On ∧ dom 𝐹 ∈ 𝐶 ) → dom 𝐹 ⊆ 𝐶 )
17	16	adantrl	⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → dom 𝐹 ⊆ 𝐶 )
18	17	3adant3	⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ∧ 𝑏 ∈ 𝐵 ) → dom 𝐹 ⊆ 𝐶 )
19	1	oismo	⊢ ( 𝐵 ⊆ On → ( Smo 𝐹 ∧ ran 𝐹 = 𝐵 ) )
20	3 19	syl	⊢ ( 𝐵 ∈ 𝒫 On → ( Smo 𝐹 ∧ ran 𝐹 = 𝐵 ) )
21	20	ad2antrl	⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( Smo 𝐹 ∧ ran 𝐹 = 𝐵 ) )
22	21	simprd	⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ran 𝐹 = 𝐵 )
23	1	oif	⊢ 𝐹 : dom 𝐹 ⟶ 𝐵
24	22 23	jctil	⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) )
25		dffo2	⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐵 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ran 𝐹 = 𝐵 ) )
26	24 25	sylibr	⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → 𝐹 : dom 𝐹 –onto→ 𝐵 )
27		dffo3	⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐵 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ dom 𝐹 𝑏 = ( 𝐹 ‘ 𝑒 ) ) )
28	27	simprbi	⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐵 → ∀ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ dom 𝐹 𝑏 = ( 𝐹 ‘ 𝑒 ) )
29		rsp	⊢ ( ∀ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ dom 𝐹 𝑏 = ( 𝐹 ‘ 𝑒 ) → ( 𝑏 ∈ 𝐵 → ∃ 𝑒 ∈ dom 𝐹 𝑏 = ( 𝐹 ‘ 𝑒 ) ) )
30	26 28 29	3syl	⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( 𝑏 ∈ 𝐵 → ∃ 𝑒 ∈ dom 𝐹 𝑏 = ( 𝐹 ‘ 𝑒 ) ) )
31	30	3impia	⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ∧ 𝑏 ∈ 𝐵 ) → ∃ 𝑒 ∈ dom 𝐹 𝑏 = ( 𝐹 ‘ 𝑒 ) )
32		ssrexv	⊢ ( dom 𝐹 ⊆ 𝐶 → ( ∃ 𝑒 ∈ dom 𝐹 𝑏 = ( 𝐹 ‘ 𝑒 ) → ∃ 𝑒 ∈ 𝐶 𝑏 = ( 𝐹 ‘ 𝑒 ) ) )
33	18 31 32	sylc	⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ∧ 𝑏 ∈ 𝐵 ) → ∃ 𝑒 ∈ 𝐶 𝑏 = ( 𝐹 ‘ 𝑒 ) )
34	33	3exp	⊢ ( 𝐶 ∈ On → ( ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) → ( 𝑏 ∈ 𝐵 → ∃ 𝑒 ∈ 𝐶 𝑏 = ( 𝐹 ‘ 𝑒 ) ) ) )
35	14 34	sylan9r	⊢ ( ( 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( 𝑎 ∈ 𝐴 → ( 𝑏 ∈ 𝐵 → ∃ 𝑒 ∈ 𝐶 𝑏 = ( 𝐹 ‘ 𝑒 ) ) ) )
36	13 35	reximdai	⊢ ( ( 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( ∃ 𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑒 ∈ 𝐶 𝑏 = ( 𝐹 ‘ 𝑒 ) ) )
37	36	3adant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( ∃ 𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑒 ∈ 𝐶 𝑏 = ( 𝐹 ‘ 𝑒 ) ) )
38		nfv	⊢ Ⅎ 𝑑 ∃ 𝑒 ∈ 𝐶 𝑏 = ( 𝐹 ‘ 𝑒 )
39		nfcv	⊢ Ⅎ 𝑎 𝐶
40		nfcv	⊢ Ⅎ 𝑎 E
41		nfcsb1v	⊢ Ⅎ 𝑎 ⦋ 𝑑 / 𝑎 ⦌ 𝐵
42	40 41	nfoi	⊢ Ⅎ 𝑎 OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 )
43		nfcv	⊢ Ⅎ 𝑎 𝑒
44	42 43	nffv	⊢ Ⅎ 𝑎 ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 )
45	44	nfeq2	⊢ Ⅎ 𝑎 𝑏 = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 )
46	39 45	nfrex	⊢ Ⅎ 𝑎 ∃ 𝑒 ∈ 𝐶 𝑏 = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 )
47		csbeq1a	⊢ ( 𝑎 = 𝑑 → 𝐵 = ⦋ 𝑑 / 𝑎 ⦌ 𝐵 )
48		oieq2	⊢ ( 𝐵 = ⦋ 𝑑 / 𝑎 ⦌ 𝐵 → OrdIso ( E , 𝐵 ) = OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) )
49	47 48	syl	⊢ ( 𝑎 = 𝑑 → OrdIso ( E , 𝐵 ) = OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) )
50	1 49	syl5eq	⊢ ( 𝑎 = 𝑑 → 𝐹 = OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) )
51	50	fveq1d	⊢ ( 𝑎 = 𝑑 → ( 𝐹 ‘ 𝑒 ) = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 ) )
52	51	eqeq2d	⊢ ( 𝑎 = 𝑑 → ( 𝑏 = ( 𝐹 ‘ 𝑒 ) ↔ 𝑏 = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 ) ) )
53	52	rexbidv	⊢ ( 𝑎 = 𝑑 → ( ∃ 𝑒 ∈ 𝐶 𝑏 = ( 𝐹 ‘ 𝑒 ) ↔ ∃ 𝑒 ∈ 𝐶 𝑏 = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 ) ) )
54	38 46 53	cbvrexw	⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑒 ∈ 𝐶 𝑏 = ( 𝐹 ‘ 𝑒 ) ↔ ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐶 𝑏 = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 ) )
55	37 54	syl6ib	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( ∃ 𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 → ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐶 𝑏 = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 ) ) )
56		eliun	⊢ ( 𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 ↔ ∃ 𝑎 ∈ 𝐴 𝑏 ∈ 𝐵 )
57		vex	⊢ 𝑑 ∈ V
58		vex	⊢ 𝑒 ∈ V
59	57 58	op1std	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑒 ⟩ → ( 1st ‘ 𝑐 ) = 𝑑 )
60	59	csbeq1d	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑒 ⟩ → ⦋ ( 1st ‘ 𝑐 ) / 𝑎 ⦌ 𝐵 = ⦋ 𝑑 / 𝑎 ⦌ 𝐵 )
61		oieq2	⊢ ( ⦋ ( 1st ‘ 𝑐 ) / 𝑎 ⦌ 𝐵 = ⦋ 𝑑 / 𝑎 ⦌ 𝐵 → OrdIso ( E , ⦋ ( 1st ‘ 𝑐 ) / 𝑎 ⦌ 𝐵 ) = OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) )
62	60 61	syl	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑒 ⟩ → OrdIso ( E , ⦋ ( 1st ‘ 𝑐 ) / 𝑎 ⦌ 𝐵 ) = OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) )
63	57 58	op2ndd	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑒 ⟩ → ( 2nd ‘ 𝑐 ) = 𝑒 )
64	62 63	fveq12d	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑒 ⟩ → ( OrdIso ( E , ⦋ ( 1st ‘ 𝑐 ) / 𝑎 ⦌ 𝐵 ) ‘ ( 2nd ‘ 𝑐 ) ) = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 ) )
65	64	eqeq2d	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑒 ⟩ → ( 𝑏 = ( OrdIso ( E , ⦋ ( 1st ‘ 𝑐 ) / 𝑎 ⦌ 𝐵 ) ‘ ( 2nd ‘ 𝑐 ) ) ↔ 𝑏 = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 ) ) )
66	65	rexxp	⊢ ( ∃ 𝑐 ∈ ( 𝐴 × 𝐶 ) 𝑏 = ( OrdIso ( E , ⦋ ( 1st ‘ 𝑐 ) / 𝑎 ⦌ 𝐵 ) ‘ ( 2nd ‘ 𝑐 ) ) ↔ ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐶 𝑏 = ( OrdIso ( E , ⦋ 𝑑 / 𝑎 ⦌ 𝐵 ) ‘ 𝑒 ) )
67	55 56 66	3imtr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ( 𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 → ∃ 𝑐 ∈ ( 𝐴 × 𝐶 ) 𝑏 = ( OrdIso ( E , ⦋ ( 1st ‘ 𝑐 ) / 𝑎 ⦌ 𝐵 ) ‘ ( 2nd ‘ 𝑐 ) ) ) )
68	67	imp	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) ∧ 𝑏 ∈ ∪ 𝑎 ∈ 𝐴 𝐵 ) → ∃ 𝑐 ∈ ( 𝐴 × 𝐶 ) 𝑏 = ( OrdIso ( E , ⦋ ( 1st ‘ 𝑐 ) / 𝑎 ⦌ 𝐵 ) ‘ ( 2nd ‘ 𝑐 ) ) )
69	10 68	wdomd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → ∪ 𝑎 ∈ 𝐴 𝐵 ≼* ( 𝐴 × 𝐶 ) )
70	2	hsmexlem1	⊢ ( ( ∪ 𝑎 ∈ 𝐴 𝐵 ⊆ On ∧ ∪ 𝑎 ∈ 𝐴 𝐵 ≼* ( 𝐴 × 𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) )
71	8 69 70	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀ 𝑎 ∈ 𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) )