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 10386

Description: Lemma for hsmex 10389. 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 6867	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘∅))
3	2	imaeq2d 6049	. . . . . . . 8 ⊢ (𝑐 = ∅ → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘∅)))
4		oieq2 9461	. . . . . . . 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 2809	. . . . . 6 ⊢ (𝑐 = ∅ → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
7	6	dmeqd 5881	. . . . 5 ⊢ (𝑐 = ∅ → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
8		fveq2 6867	. . . . 5 ⊢ (𝑐 = ∅ → (𝐻‘𝑐) = (𝐻‘∅))
9	7, 8	eleq12d 2856	. . . 4 ⊢ (𝑐 = ∅ → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
10	9	ralbidv 3185	. . 3 ⊢ (𝑐 = ∅ → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
11		fveq2 6867	. . . . . . . . 9 ⊢ (𝑐 = 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘𝑒))
12	11	imaeq2d 6049	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘𝑒)))
13		oieq2 9461	. . . . . . . 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 2809	. . . . . 6 ⊢ (𝑐 = 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
16	15	dmeqd 5881	. . . . 5 ⊢ (𝑐 = 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
17		fveq2 6867	. . . . 5 ⊢ (𝑐 = 𝑒 → (𝐻‘𝑐) = (𝐻‘𝑒))
18	16, 17	eleq12d 2856	. . . 4 ⊢ (𝑐 = 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
19	18	ralbidv 3185	. . 3 ⊢ (𝑐 = 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
20		fveq2 6867	. . . . . . . . 9 ⊢ (𝑐 = suc 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘suc 𝑒))
21	20	imaeq2d 6049	. . . . . . . 8 ⊢ (𝑐 = suc 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘suc 𝑒)))
22		oieq2 9461	. . . . . . . 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 2809	. . . . . 6 ⊢ (𝑐 = suc 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
25	24	dmeqd 5881	. . . . 5 ⊢ (𝑐 = suc 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
26		fveq2 6867	. . . . 5 ⊢ (𝑐 = suc 𝑒 → (𝐻‘𝑐) = (𝐻‘suc 𝑒))
27	25, 26	eleq12d 2856	. . . 4 ⊢ (𝑐 = suc 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
28	27	ralbidv 3185	. . 3 ⊢ (𝑐 = suc 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
29		imassrn 6060	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) ⊆ ran rank
30		rankf 9752	. . . . . . . 8 ⊢ rank:∪ (𝑅₁ “ On)⟶On
31		frn 6699	. . . . . . . 8 ⊢ (rank:∪ (𝑅₁ “ On)⟶On → ran rank ⊆ On)
32	30, 31	ax-mp 5	. . . . . . 7 ⊢ ran rank ⊆ On
33	29, 32	sstri 3945	. . . . . 6 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) ⊆ On
34		hsmexlem4.u	. . . . . . . . . 10 ⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω))
35	34	ituni0 10375	. . . . . . . . 9 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘∅) = 𝑑)
36	35	elv 3459	. . . . . . . 8 ⊢ ((𝑈‘𝑑)‘∅) = 𝑑
37	36	imaeq2i 6047	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) = (rank “ 𝑑)
38		ffun 6694	. . . . . . . . . 10 ⊢ (rank:∪ (𝑅₁ “ On)⟶On → Fun rank)
39	30, 38	ax-mp 5	. . . . . . . . 9 ⊢ Fun rank
40		vex 3458	. . . . . . . . 9 ⊢ 𝑑 ∈ V
41		wdomimag 9535	. . . . . . . . 9 ⊢ ((Fun rank ∧ 𝑑 ∈ V) → (rank “ 𝑑) ≼^* 𝑑)
42	39, 40, 41	mp2an 702	. . . . . . . 8 ⊢ (rank “ 𝑑) ≼^* 𝑑
43		sneq 4592	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑})
44	43	fveq2d 6871	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (TC‘{𝑎}) = (TC‘{𝑑}))
45	44	raleqdv 3320	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
46		hsmexlem4.s	. . . . . . . . . . 11 ⊢ 𝑆 = {𝑎 ∈ ∪ (𝑅₁ “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋}
47	45, 46	elrab2 3654	. . . . . . . . . 10 ⊢ (𝑑 ∈ 𝑆 ↔ (𝑑 ∈ ∪ (𝑅₁ “ On) ∧ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
48	47	simprbi 501	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝑆 → ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋)
49		vsnex 5392	. . . . . . . . . . . 12 ⊢ {𝑑} ∈ V
50		tcid 9692	. . . . . . . . . . . 12 ⊢ ({𝑑} ∈ V → {𝑑} ⊆ (TC‘{𝑑}))
51	49, 50	ax-mp 5	. . . . . . . . . . 11 ⊢ {𝑑} ⊆ (TC‘{𝑑})
52		vsnid 4622	. . . . . . . . . . 11 ⊢ 𝑑 ∈ {𝑑}
53	51, 52	sselii 3933	. . . . . . . . . 10 ⊢ 𝑑 ∈ (TC‘{𝑑})
54		breq1 5103	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ≼ 𝑋 ↔ 𝑑 ≼ 𝑋))
55	54	rspcv 3577	. . . . . . . . . 10 ⊢ (𝑑 ∈ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋))
56	53, 55	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋)
57		domwdom 9522	. . . . . . . . 9 ⊢ (𝑑 ≼ 𝑋 → 𝑑 ≼^* 𝑋)
58	48, 56, 57	3syl 18	. . . . . . . 8 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ≼^* 𝑋)
59		wdomtr 9523	. . . . . . . 8 ⊢ (((rank “ 𝑑) ≼^* 𝑑 ∧ 𝑑 ≼^* 𝑋) → (rank “ 𝑑) ≼^* 𝑋)
60	42, 58, 59	sylancr 596	. . . . . . 7 ⊢ (𝑑 ∈ 𝑆 → (rank “ 𝑑) ≼^* 𝑋)
61	37, 60	eqbrtrid 5135	. . . . . 6 ⊢ (𝑑 ∈ 𝑆 → (rank “ ((𝑈‘𝑑)‘∅)) ≼^* 𝑋)
62		eqid 2762	. . . . . . 7 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅)))
63	62	hsmexlem1 10383	. . . . . 6 ⊢ (((rank “ ((𝑈‘𝑑)‘∅)) ⊆ On ∧ (rank “ ((𝑈‘𝑑)‘∅)) ≼^* 𝑋) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
64	33, 61, 63	sylancr 596	. . . . 5 ⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
65		hsmexlem4.h	. . . . . 6 ⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω)
66	65	hsmexlem7 10380	. . . . 5 ⊢ (𝐻‘∅) = (har‘𝒫 𝑋)
67	64, 66	eleqtrrdi 2873	. . . 4 ⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅))
68	67	rgen 3078	. . 3 ⊢ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)
69		nfra1 3286	. . . . . 6 ⊢ Ⅎ𝑑∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)
70		nfv 1934	. . . . . 6 ⊢ Ⅎ𝑑 𝑒 ∈ ω
71	69, 70	nfan 1919	. . . . 5 ⊢ Ⅎ𝑑(∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω)
72	34	ituniiun 10379	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
73	72	elv 3459	. . . . . . . . . . . 12 ⊢ ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)
74	73	imaeq2i 6047	. . . . . . . . . . 11 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
75		imaiun 7229	. . . . . . . . . . 11 ⊢ (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
76	74, 75	eqtri 2785	. . . . . . . . . 10 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
77		oieq2 9461	. . . . . . . . . 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 5880	. . . . . . . 8 ⊢ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
80	58	ad2antll 739	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → 𝑑 ≼^* 𝑋)
81	65	hsmexlem9 10382	. . . . . . . . . 10 ⊢ (𝑒 ∈ ω → (𝐻‘𝑒) ∈ On)
82	81	ad2antrl 738	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘𝑒) ∈ On)
83		fveq2 6867	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑓 → (𝑈‘𝑑) = (𝑈‘𝑓))
84	83	fveq1d 6869	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑓 → ((𝑈‘𝑑)‘𝑒) = ((𝑈‘𝑓)‘𝑒))
85	84	imaeq2d 6049	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑓 → (rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)))
86		oieq2 9461	. . . . . . . . . . . . . . 15 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
87	85, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑓 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
88	87	dmeqd 5881	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑓 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
89	88	eleq1d 2847	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑓 → (dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
90		simpll 776	. . . . . . . . . . . 12 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒))
91	46	ssrab3 4035	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 ⊆ ∪ (𝑅₁ “ On)
92	91	sseli 3932	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ∈ ∪ (𝑅₁ “ On))
93		r1elssi 9763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ ∪ (𝑅₁ “ On) → 𝑑 ⊆ ∪ (𝑅₁ “ On))
94	92, 93	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ⊆ ∪ (𝑅₁ “ On))
95	94	sselda 3936	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ ∪ (𝑅₁ “ On))
96		snssi 4744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ 𝑑 → {𝑓} ⊆ 𝑑)
97	40	tcss 9697	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑓} ⊆ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
99	49	tcel 9698	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ {𝑑} → (TC‘𝑑) ⊆ (TC‘{𝑑}))
100	52, 99	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘𝑑) ⊆ (TC‘{𝑑}))
101	98, 100	sstrd 3946	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘{𝑑}))
102		ssralv 4005	. . . . . . . . . . . . . . . . 17 ⊢ ((TC‘{𝑓}) ⊆ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
103	101, 102	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ 𝑑 → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
104	48, 103	mpan9 514	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋)
105		sneq 4592	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑓 → {𝑎} = {𝑓})
106	105	fveq2d 6871	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑓 → (TC‘{𝑎}) = (TC‘{𝑓}))
107	106	raleqdv 3320	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑓 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
108	107, 46	elrab2 3654	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ ∪ (𝑅₁ “ On) ∧ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
109	95, 104, 108	sylanbrc 592	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
110	109	adantll 724	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
111	110	adantll 724	. . . . . . . . . . . 12 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
112	89, 90, 111	rspcdva 3582	. . . . . . . . . . 11 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))
113		imassrn 6060	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ ran rank
114	113, 32	sstri 3945	. . . . . . . . . . . 12 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ On
115		fvex 6880	. . . . . . . . . . . . . . 15 ⊢ ((𝑈‘𝑓)‘𝑒) ∈ V
116	115	funimaex 6609	. . . . . . . . . . . . . 14 ⊢ (Fun rank → (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V)
117	39, 116	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V
118	117	elpw 4559	. . . . . . . . . . . 12 ⊢ ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ↔ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ On)
119	114, 118	mpbir 233	. . . . . . . . . . 11 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On
120	112, 119	jctil 527	. . . . . . . . . 10 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
121	120	ralrimiva 3154	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
122		eqid 2762	. . . . . . . . . 10 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒)))
123		eqid 2762	. . . . . . . . . 10 ⊢ OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
124	122, 123	hsmexlem3 10385	. . . . . . . . 9 ⊢ (((𝑑 ≼^* 𝑋 ∧ (𝐻‘𝑒) ∈ On) ∧ ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
125	80, 82, 121, 124	syl21anc 848	. . . . . . . 8 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
126	79, 125	eqeltrid 2866	. . . . . . 7 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
127	65	hsmexlem8 10381	. . . . . . . 8 ⊢ (𝑒 ∈ ω → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
128	127	ad2antrl 738	. . . . . . 7 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
129	126, 128	eleqtrrd 2865	. . . . . 6 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
130	129	expr 460	. . . . 5 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω) → (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
131	71, 130	ralrimi 3260	. . . 4 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
132	131	expcom 417	. . 3 ⊢ (𝑒 ∈ ω → (∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
133	10, 19, 28, 68, 132	finds1 7880	. 2 ⊢ (𝑐 ∈ ω → ∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐))
134	133	r19.21bi 3254	1 ⊢ ((𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆) → dom 𝑂 ∈ (𝐻‘𝑐))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1560 ∈ wcel 2142 ∀wral 3076 {crab 3414 Vcvv 3454 ⊆ wss 3904 ∅c0 4285 𝒫 cpw 4555 {csn 4582 ∪ cuni 4865 ∪ ciun 4949 class class class wbr 5100 ↦ cmpt 5181 E cep 5546 × cxp 5645 dom cdm 5647 ran crn 5648 ↾ cres 5649 “ cima 5650 Oncon0 6346 suc csuc 6348 Fun wfun 6515 ⟶wf 6517 ‘cfv 6521 ωcom 7846 reccrdg 8380 ≼ cdom 8925 OrdIsocoi 9457 harchar 9504 ≼^* cwdom 9512 TCctc 9689 𝑅₁cr1 9720 rankcrnk 9721

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-inf2 9596

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-om 7847 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-smo 8317 df-recs 8342 df-rdg 8381 df-en 8928 df-dom 8929 df-sdom 8930 df-oi 9458 df-har 9505 df-wdom 9513 df-tc 9690 df-r1 9722 df-rank 9723

This theorem is referenced by: hsmexlem5 10387

W3C validator