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 10351

Description: Lemma for hsmex 10354. 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 6842	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘∅))
3	2	imaeq2d 6027	. . . . . . . 8 ⊢ (𝑐 = ∅ → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘∅)))
4		oieq2 9430	. . . . . . . 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 5862	. . . . 5 ⊢ (𝑐 = ∅ → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
8		fveq2 6842	. . . . 5 ⊢ (𝑐 = ∅ → (𝐻‘𝑐) = (𝐻‘∅))
9	7, 8	eleq12d 2831	. . . 4 ⊢ (𝑐 = ∅ → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
10	9	ralbidv 3161	. . 3 ⊢ (𝑐 = ∅ → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
11		fveq2 6842	. . . . . . . . 9 ⊢ (𝑐 = 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘𝑒))
12	11	imaeq2d 6027	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘𝑒)))
13		oieq2 9430	. . . . . . . 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 5862	. . . . 5 ⊢ (𝑐 = 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
17		fveq2 6842	. . . . 5 ⊢ (𝑐 = 𝑒 → (𝐻‘𝑐) = (𝐻‘𝑒))
18	16, 17	eleq12d 2831	. . . 4 ⊢ (𝑐 = 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
19	18	ralbidv 3161	. . 3 ⊢ (𝑐 = 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
20		fveq2 6842	. . . . . . . . 9 ⊢ (𝑐 = suc 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘suc 𝑒))
21	20	imaeq2d 6027	. . . . . . . 8 ⊢ (𝑐 = suc 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘suc 𝑒)))
22		oieq2 9430	. . . . . . . 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 5862	. . . . 5 ⊢ (𝑐 = suc 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
26		fveq2 6842	. . . . 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 6038	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) ⊆ ran rank
30		rankf 9718	. . . . . . . 8 ⊢ rank:∪ (𝑅₁ “ On)⟶On
31		frn 6677	. . . . . . . 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 10340	. . . . . . . . 9 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘∅) = 𝑑)
36	35	elv 3447	. . . . . . . 8 ⊢ ((𝑈‘𝑑)‘∅) = 𝑑
37	36	imaeq2i 6025	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) = (rank “ 𝑑)
38		ffun 6673	. . . . . . . . . 10 ⊢ (rank:∪ (𝑅₁ “ On)⟶On → Fun rank)
39	30, 38	ax-mp 5	. . . . . . . . 9 ⊢ Fun rank
40		vex 3446	. . . . . . . . 9 ⊢ 𝑑 ∈ V
41		wdomimag 9504	. . . . . . . . 9 ⊢ ((Fun rank ∧ 𝑑 ∈ V) → (rank “ 𝑑) ≼^* 𝑑)
42	39, 40, 41	mp2an 693	. . . . . . . 8 ⊢ (rank “ 𝑑) ≼^* 𝑑
43		sneq 4592	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑})
44	43	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (TC‘{𝑎}) = (TC‘{𝑑}))
45	44	raleqdv 3298	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
46		hsmexlem4.s	. . . . . . . . . . 11 ⊢ 𝑆 = {𝑎 ∈ ∪ (𝑅₁ “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋}
47	45, 46	elrab2 3651	. . . . . . . . . 10 ⊢ (𝑑 ∈ 𝑆 ↔ (𝑑 ∈ ∪ (𝑅₁ “ On) ∧ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
48	47	simprbi 497	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝑆 → ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋)
49		vsnex 5381	. . . . . . . . . . . 12 ⊢ {𝑑} ∈ V
50		tcid 9658	. . . . . . . . . . . 12 ⊢ ({𝑑} ∈ V → {𝑑} ⊆ (TC‘{𝑑}))
51	49, 50	ax-mp 5	. . . . . . . . . . 11 ⊢ {𝑑} ⊆ (TC‘{𝑑})
52		vsnid 4622	. . . . . . . . . . 11 ⊢ 𝑑 ∈ {𝑑}
53	51, 52	sselii 3932	. . . . . . . . . 10 ⊢ 𝑑 ∈ (TC‘{𝑑})
54		breq1 5103	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ≼ 𝑋 ↔ 𝑑 ≼ 𝑋))
55	54	rspcv 3574	. . . . . . . . . 10 ⊢ (𝑑 ∈ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋))
56	53, 55	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋)
57		domwdom 9491	. . . . . . . . 9 ⊢ (𝑑 ≼ 𝑋 → 𝑑 ≼^* 𝑋)
58	48, 56, 57	3syl 18	. . . . . . . 8 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ≼^* 𝑋)
59		wdomtr 9492	. . . . . . . 8 ⊢ (((rank “ 𝑑) ≼^* 𝑑 ∧ 𝑑 ≼^* 𝑋) → (rank “ 𝑑) ≼^* 𝑋)
60	42, 58, 59	sylancr 588	. . . . . . 7 ⊢ (𝑑 ∈ 𝑆 → (rank “ 𝑑) ≼^* 𝑋)
61	37, 60	eqbrtrid 5135	. . . . . 6 ⊢ (𝑑 ∈ 𝑆 → (rank “ ((𝑈‘𝑑)‘∅)) ≼^* 𝑋)
62		eqid 2737	. . . . . . 7 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅)))
63	62	hsmexlem1 10348	. . . . . 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 10345	. . . . 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 10344	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
73	72	elv 3447	. . . . . . . . . . . 12 ⊢ ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)
74	73	imaeq2i 6025	. . . . . . . . . . 11 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
75		imaiun 7201	. . . . . . . . . . 11 ⊢ (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
76	74, 75	eqtri 2760	. . . . . . . . . 10 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
77		oieq2 9430	. . . . . . . . . 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 5861	. . . . . . . 8 ⊢ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
80	58	ad2antll 730	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → 𝑑 ≼^* 𝑋)
81	65	hsmexlem9 10347	. . . . . . . . . 10 ⊢ (𝑒 ∈ ω → (𝐻‘𝑒) ∈ On)
82	81	ad2antrl 729	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘𝑒) ∈ On)
83		fveq2 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑓 → (𝑈‘𝑑) = (𝑈‘𝑓))
84	83	fveq1d 6844	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑓 → ((𝑈‘𝑑)‘𝑒) = ((𝑈‘𝑓)‘𝑒))
85	84	imaeq2d 6027	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑓 → (rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)))
86		oieq2 9430	. . . . . . . . . . . . . . 15 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
87	85, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑓 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
88	87	dmeqd 5862	. . . . . . . . . . . . 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 4036	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 ⊆ ∪ (𝑅₁ “ On)
92	91	sseli 3931	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ∈ ∪ (𝑅₁ “ On))
93		r1elssi 9729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ ∪ (𝑅₁ “ On) → 𝑑 ⊆ ∪ (𝑅₁ “ On))
94	92, 93	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ⊆ ∪ (𝑅₁ “ On))
95	94	sselda 3935	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ ∪ (𝑅₁ “ On))
96		snssi 4766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ 𝑑 → {𝑓} ⊆ 𝑑)
97	40	tcss 9663	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑓} ⊆ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
99	49	tcel 9664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ {𝑑} → (TC‘𝑑) ⊆ (TC‘{𝑑}))
100	52, 99	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘𝑑) ⊆ (TC‘{𝑑}))
101	98, 100	sstrd 3946	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘{𝑑}))
102		ssralv 4004	. . . . . . . . . . . . . . . . 17 ⊢ ((TC‘{𝑓}) ⊆ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
103	101, 102	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ 𝑑 → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
104	48, 103	mpan9 506	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋)
105		sneq 4592	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑓 → {𝑎} = {𝑓})
106	105	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑓 → (TC‘{𝑎}) = (TC‘{𝑓}))
107	106	raleqdv 3298	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑓 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
108	107, 46	elrab2 3651	. . . . . . . . . . . . . . 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 3579	. . . . . . . . . . 11 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))
113		imassrn 6038	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ ran rank
114	113, 32	sstri 3945	. . . . . . . . . . . 12 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ On
115		fvex 6855	. . . . . . . . . . . . . . 15 ⊢ ((𝑈‘𝑓)‘𝑒) ∈ V
116	115	funimaex 6588	. . . . . . . . . . . . . 14 ⊢ (Fun rank → (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V)
117	39, 116	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V
118	117	elpw 4560	. . . . . . . . . . . 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 10350	. . . . . . . . 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 10346	. . . . . . . 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 7851	. 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 3401 Vcvv 3442 ⊆ wss 3903 ∅c0 4287 𝒫 cpw 4556 {csn 4582 ∪ cuni 4865 ∪ ciun 4948 class class class wbr 5100 ↦ cmpt 5181 E cep 5531 × cxp 5630 dom cdm 5632 ran crn 5633 ↾ cres 5634 “ cima 5635 Oncon0 6325 suc csuc 6327 Fun wfun 6494 ⟶wf 6496 ‘cfv 6500 ωcom 7818 reccrdg 8350 ≼ cdom 8893 OrdIsocoi 9426 harchar 9473 ≼^* cwdom 9481 TCctc 9655 𝑅₁cr1 9686 rankcrnk 9687

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 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562

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 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-smo 8288 df-recs 8313 df-rdg 8351 df-en 8896 df-dom 8897 df-sdom 8898 df-oi 9427 df-har 9474 df-wdom 9482 df-tc 9656 df-r1 9688 df-rank 9689

This theorem is referenced by: hsmexlem5 10352

W3C validator