hsmexlem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hsmexlem4		Structured version Visualization version GIF version

Theorem hsmexlem4 10345

Description: Lemma for hsmex 10348. The core induction, establishing bounds on the order types of iterated unions of the initial set. (Contributed by Stefan O'Rear, 14-Feb-2015.)

**Hypotheses**
Ref	Expression
hsmexlem4.x	⊢ 𝑋 ∈ V
hsmexlem4.h	⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω)
hsmexlem4.u	⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω))
hsmexlem4.s	⊢ 𝑆 = {𝑎 ∈ ∪ (𝑅₁ “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋}
hsmexlem4.o	⊢ 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐)))

**Assertion**
Ref	Expression
hsmexlem4	⊢ ((𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆) → dom 𝑂 ∈ (𝐻‘𝑐))

Distinct variable groups: 𝑎,𝑐,𝑑,𝐻 𝑆,𝑐,𝑑 𝑈,𝑐,𝑑 𝑎,𝑏,𝑧,𝑋 𝑥,𝑎,𝑦 𝑏,𝑐,𝑑,𝑥,𝑦,𝑧 Allowed substitution hints: 𝑆(𝑥,𝑦,𝑧,𝑎,𝑏) 𝑈(𝑥,𝑦,𝑧,𝑎,𝑏) 𝐻(𝑥,𝑦,𝑧,𝑏) 𝑂(𝑥,𝑦,𝑧,𝑎,𝑏,𝑐,𝑑) 𝑋(𝑥,𝑦,𝑐,𝑑)

Proof of Theorem hsmexlem4 Dummy variables 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hsmexlem4.o	. . . . . . 7 ⊢ 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐)))
2		fveq2 6835	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘∅))
3	2	imaeq2d 6020	. . . . . . . 8 ⊢ (𝑐 = ∅ → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘∅)))
4		oieq2 9422	. . . . . . . 8 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘∅)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝑐 = ∅ → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
6	1, 5	eqtrid 2784	. . . . . 6 ⊢ (𝑐 = ∅ → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
7	6	dmeqd 5855	. . . . 5 ⊢ (𝑐 = ∅ → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
8		fveq2 6835	. . . . 5 ⊢ (𝑐 = ∅ → (𝐻‘𝑐) = (𝐻‘∅))
9	7, 8	eleq12d 2831	. . . 4 ⊢ (𝑐 = ∅ → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
10	9	ralbidv 3161	. . 3 ⊢ (𝑐 = ∅ → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
11		fveq2 6835	. . . . . . . . 9 ⊢ (𝑐 = 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘𝑒))
12	11	imaeq2d 6020	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘𝑒)))
13		oieq2 9422	. . . . . . . 8 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
14	12, 13	syl 17	. . . . . . 7 ⊢ (𝑐 = 𝑒 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
15	1, 14	eqtrid 2784	. . . . . 6 ⊢ (𝑐 = 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
16	15	dmeqd 5855	. . . . 5 ⊢ (𝑐 = 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
17		fveq2 6835	. . . . 5 ⊢ (𝑐 = 𝑒 → (𝐻‘𝑐) = (𝐻‘𝑒))
18	16, 17	eleq12d 2831	. . . 4 ⊢ (𝑐 = 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
19	18	ralbidv 3161	. . 3 ⊢ (𝑐 = 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
20		fveq2 6835	. . . . . . . . 9 ⊢ (𝑐 = suc 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘suc 𝑒))
21	20	imaeq2d 6020	. . . . . . . 8 ⊢ (𝑐 = suc 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘suc 𝑒)))
22		oieq2 9422	. . . . . . . 8 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘suc 𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
23	21, 22	syl 17	. . . . . . 7 ⊢ (𝑐 = suc 𝑒 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
24	1, 23	eqtrid 2784	. . . . . 6 ⊢ (𝑐 = suc 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
25	24	dmeqd 5855	. . . . 5 ⊢ (𝑐 = suc 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
26		fveq2 6835	. . . . 5 ⊢ (𝑐 = suc 𝑒 → (𝐻‘𝑐) = (𝐻‘suc 𝑒))
27	25, 26	eleq12d 2831	. . . 4 ⊢ (𝑐 = suc 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
28	27	ralbidv 3161	. . 3 ⊢ (𝑐 = suc 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
29		imassrn 6031	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) ⊆ ran rank
30		rankf 9712	. . . . . . . 8 ⊢ rank:∪ (𝑅₁ “ On)⟶On
31		frn 6670	. . . . . . . 8 ⊢ (rank:∪ (𝑅₁ “ On)⟶On → ran rank ⊆ On)
32	30, 31	ax-mp 5	. . . . . . 7 ⊢ ran rank ⊆ On
33	29, 32	sstri 3932	. . . . . 6 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) ⊆ On
34		hsmexlem4.u	. . . . . . . . . 10 ⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω))
35	34	ituni0 10334	. . . . . . . . 9 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘∅) = 𝑑)
36	35	elv 3435	. . . . . . . 8 ⊢ ((𝑈‘𝑑)‘∅) = 𝑑
37	36	imaeq2i 6018	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) = (rank “ 𝑑)
38		ffun 6666	. . . . . . . . . 10 ⊢ (rank:∪ (𝑅₁ “ On)⟶On → Fun rank)
39	30, 38	ax-mp 5	. . . . . . . . 9 ⊢ Fun rank
40		vex 3434	. . . . . . . . 9 ⊢ 𝑑 ∈ V
41		wdomimag 9496	. . . . . . . . 9 ⊢ ((Fun rank ∧ 𝑑 ∈ V) → (rank “ 𝑑) ≼^* 𝑑)
42	39, 40, 41	mp2an 693	. . . . . . . 8 ⊢ (rank “ 𝑑) ≼^* 𝑑
43		sneq 4578	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑})
44	43	fveq2d 6839	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (TC‘{𝑎}) = (TC‘{𝑑}))
45	44	raleqdv 3296	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
46		hsmexlem4.s	. . . . . . . . . . 11 ⊢ 𝑆 = {𝑎 ∈ ∪ (𝑅₁ “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋}
47	45, 46	elrab2 3638	. . . . . . . . . 10 ⊢ (𝑑 ∈ 𝑆 ↔ (𝑑 ∈ ∪ (𝑅₁ “ On) ∧ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
48	47	simprbi 497	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝑆 → ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋)
49		vsnex 5373	. . . . . . . . . . . 12 ⊢ {𝑑} ∈ V
50		tcid 9652	. . . . . . . . . . . 12 ⊢ ({𝑑} ∈ V → {𝑑} ⊆ (TC‘{𝑑}))
51	49, 50	ax-mp 5	. . . . . . . . . . 11 ⊢ {𝑑} ⊆ (TC‘{𝑑})
52		vsnid 4608	. . . . . . . . . . 11 ⊢ 𝑑 ∈ {𝑑}
53	51, 52	sselii 3919	. . . . . . . . . 10 ⊢ 𝑑 ∈ (TC‘{𝑑})
54		breq1 5089	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ≼ 𝑋 ↔ 𝑑 ≼ 𝑋))
55	54	rspcv 3561	. . . . . . . . . 10 ⊢ (𝑑 ∈ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋))
56	53, 55	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋)
57		domwdom 9483	. . . . . . . . 9 ⊢ (𝑑 ≼ 𝑋 → 𝑑 ≼^* 𝑋)
58	48, 56, 57	3syl 18	. . . . . . . 8 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ≼^* 𝑋)
59		wdomtr 9484	. . . . . . . 8 ⊢ (((rank “ 𝑑) ≼^* 𝑑 ∧ 𝑑 ≼^* 𝑋) → (rank “ 𝑑) ≼^* 𝑋)
60	42, 58, 59	sylancr 588	. . . . . . 7 ⊢ (𝑑 ∈ 𝑆 → (rank “ 𝑑) ≼^* 𝑋)
61	37, 60	eqbrtrid 5121	. . . . . 6 ⊢ (𝑑 ∈ 𝑆 → (rank “ ((𝑈‘𝑑)‘∅)) ≼^* 𝑋)
62		eqid 2737	. . . . . . 7 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅)))
63	62	hsmexlem1 10342	. . . . . 6 ⊢ (((rank “ ((𝑈‘𝑑)‘∅)) ⊆ On ∧ (rank “ ((𝑈‘𝑑)‘∅)) ≼^* 𝑋) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
64	33, 61, 63	sylancr 588	. . . . 5 ⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
65		hsmexlem4.h	. . . . . 6 ⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω)
66	65	hsmexlem7 10339	. . . . 5 ⊢ (𝐻‘∅) = (har‘𝒫 𝑋)
67	64, 66	eleqtrrdi 2848	. . . 4 ⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅))
68	67	rgen 3054	. . 3 ⊢ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)
69		nfra1 3262	. . . . . 6 ⊢ Ⅎ𝑑∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)
70		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑑 𝑒 ∈ ω
71	69, 70	nfan 1901	. . . . 5 ⊢ Ⅎ𝑑(∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω)
72	34	ituniiun 10338	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
73	72	elv 3435	. . . . . . . . . . . 12 ⊢ ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)
74	73	imaeq2i 6018	. . . . . . . . . . 11 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
75		imaiun 7194	. . . . . . . . . . 11 ⊢ (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
76	74, 75	eqtri 2760	. . . . . . . . . 10 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
77		oieq2 9422	. . . . . . . . . 10 ⊢ ((rank “ ((𝑈‘𝑑)‘suc 𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))))
78	76, 77	ax-mp 5	. . . . . . . . 9 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
79	78	dmeqi 5854	. . . . . . . 8 ⊢ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
80	58	ad2antll 730	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → 𝑑 ≼^* 𝑋)
81	65	hsmexlem9 10341	. . . . . . . . . 10 ⊢ (𝑒 ∈ ω → (𝐻‘𝑒) ∈ On)
82	81	ad2antrl 729	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘𝑒) ∈ On)
83		fveq2 6835	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑓 → (𝑈‘𝑑) = (𝑈‘𝑓))
84	83	fveq1d 6837	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑓 → ((𝑈‘𝑑)‘𝑒) = ((𝑈‘𝑓)‘𝑒))
85	84	imaeq2d 6020	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑓 → (rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)))
86		oieq2 9422	. . . . . . . . . . . . . . 15 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
87	85, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑓 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
88	87	dmeqd 5855	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑓 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
89	88	eleq1d 2822	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑓 → (dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
90		simpll 767	. . . . . . . . . . . 12 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒))
91	46	ssrab3 4023	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 ⊆ ∪ (𝑅₁ “ On)
92	91	sseli 3918	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ∈ ∪ (𝑅₁ “ On))
93		r1elssi 9723	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ ∪ (𝑅₁ “ On) → 𝑑 ⊆ ∪ (𝑅₁ “ On))
94	92, 93	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ⊆ ∪ (𝑅₁ “ On))
95	94	sselda 3922	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ ∪ (𝑅₁ “ On))
96		snssi 4752	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ 𝑑 → {𝑓} ⊆ 𝑑)
97	40	tcss 9657	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑓} ⊆ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
99	49	tcel 9658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ {𝑑} → (TC‘𝑑) ⊆ (TC‘{𝑑}))
100	52, 99	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘𝑑) ⊆ (TC‘{𝑑}))
101	98, 100	sstrd 3933	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘{𝑑}))
102		ssralv 3991	. . . . . . . . . . . . . . . . 17 ⊢ ((TC‘{𝑓}) ⊆ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
103	101, 102	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ 𝑑 → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
104	48, 103	mpan9 506	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋)
105		sneq 4578	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑓 → {𝑎} = {𝑓})
106	105	fveq2d 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑓 → (TC‘{𝑎}) = (TC‘{𝑓}))
107	106	raleqdv 3296	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑓 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
108	107, 46	elrab2 3638	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ ∪ (𝑅₁ “ On) ∧ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
109	95, 104, 108	sylanbrc 584	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
110	109	adantll 715	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
111	110	adantll 715	. . . . . . . . . . . 12 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
112	89, 90, 111	rspcdva 3566	. . . . . . . . . . 11 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))
113		imassrn 6031	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ ran rank
114	113, 32	sstri 3932	. . . . . . . . . . . 12 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ On
115		fvex 6848	. . . . . . . . . . . . . . 15 ⊢ ((𝑈‘𝑓)‘𝑒) ∈ V
116	115	funimaex 6581	. . . . . . . . . . . . . 14 ⊢ (Fun rank → (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V)
117	39, 116	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V
118	117	elpw 4546	. . . . . . . . . . . 12 ⊢ ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ↔ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ On)
119	114, 118	mpbir 231	. . . . . . . . . . 11 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On
120	112, 119	jctil 519	. . . . . . . . . 10 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
121	120	ralrimiva 3130	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
122		eqid 2737	. . . . . . . . . 10 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒)))
123		eqid 2737	. . . . . . . . . 10 ⊢ OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
124	122, 123	hsmexlem3 10344	. . . . . . . . 9 ⊢ (((𝑑 ≼^* 𝑋 ∧ (𝐻‘𝑒) ∈ On) ∧ ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
125	80, 82, 121, 124	syl21anc 838	. . . . . . . 8 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
126	79, 125	eqeltrid 2841	. . . . . . 7 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
127	65	hsmexlem8 10340	. . . . . . . 8 ⊢ (𝑒 ∈ ω → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
128	127	ad2antrl 729	. . . . . . 7 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
129	126, 128	eleqtrrd 2840	. . . . . 6 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
130	129	expr 456	. . . . 5 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω) → (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
131	71, 130	ralrimi 3236	. . . 4 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
132	131	expcom 413	. . 3 ⊢ (𝑒 ∈ ω → (∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
133	10, 19, 28, 68, 132	finds1 7844	. 2 ⊢ (𝑐 ∈ ω → ∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐))
134	133	r19.21bi 3230	1 ⊢ ((𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆) → dom 𝑂 ∈ (𝐻‘𝑐))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 {crab 3390 Vcvv 3430 ⊆ wss 3890 ∅c0 4274 𝒫 cpw 4542 {csn 4568 ∪ cuni 4851 ∪ ciun 4934 class class class wbr 5086 ↦ cmpt 5167 E cep 5524 × cxp 5623 dom cdm 5625 ran crn 5626 ↾ cres 5627 “ cima 5628 Oncon0 6318 suc csuc 6320 Fun wfun 6487 ⟶wf 6489 ‘cfv 6493 ωcom 7811 reccrdg 8342 ≼ cdom 8885 OrdIsocoi 9418 harchar 9465 ≼^* cwdom 9473 TCctc 9649 𝑅₁cr1 9680 rankcrnk 9681

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-inf2 9556

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-om 7812 df-1st 7936 df-2nd 7937 df-frecs 8225 df-wrecs 8256 df-smo 8280 df-recs 8305 df-rdg 8343 df-en 8888 df-dom 8889 df-sdom 8890 df-oi 9419 df-har 9466 df-wdom 9474 df-tc 9650 df-r1 9682 df-rank 9683

This theorem is referenced by: hsmexlem5 10346

W3C validator