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 10441

Description: Lemma for hsmex 10444. 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 6875	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘∅))
3	2	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑐 = ∅ → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘∅)))
4		oieq2 9525	. . . . . . . 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 2782	. . . . . 6 ⊢ (𝑐 = ∅ → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
7	6	dmeqd 5885	. . . . 5 ⊢ (𝑐 = ∅ → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
8		fveq2 6875	. . . . 5 ⊢ (𝑐 = ∅ → (𝐻‘𝑐) = (𝐻‘∅))
9	7, 8	eleq12d 2828	. . . 4 ⊢ (𝑐 = ∅ → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
10	9	ralbidv 3163	. . 3 ⊢ (𝑐 = ∅ → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
11		fveq2 6875	. . . . . . . . 9 ⊢ (𝑐 = 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘𝑒))
12	11	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘𝑒)))
13		oieq2 9525	. . . . . . . 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 2782	. . . . . 6 ⊢ (𝑐 = 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
16	15	dmeqd 5885	. . . . 5 ⊢ (𝑐 = 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
17		fveq2 6875	. . . . 5 ⊢ (𝑐 = 𝑒 → (𝐻‘𝑐) = (𝐻‘𝑒))
18	16, 17	eleq12d 2828	. . . 4 ⊢ (𝑐 = 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
19	18	ralbidv 3163	. . 3 ⊢ (𝑐 = 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
20		fveq2 6875	. . . . . . . . 9 ⊢ (𝑐 = suc 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘suc 𝑒))
21	20	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑐 = suc 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘suc 𝑒)))
22		oieq2 9525	. . . . . . . 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 2782	. . . . . 6 ⊢ (𝑐 = suc 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
25	24	dmeqd 5885	. . . . 5 ⊢ (𝑐 = suc 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
26		fveq2 6875	. . . . 5 ⊢ (𝑐 = suc 𝑒 → (𝐻‘𝑐) = (𝐻‘suc 𝑒))
27	25, 26	eleq12d 2828	. . . 4 ⊢ (𝑐 = suc 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
28	27	ralbidv 3163	. . 3 ⊢ (𝑐 = suc 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
29		imassrn 6058	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) ⊆ ran rank
30		rankf 9806	. . . . . . . 8 ⊢ rank:∪ (𝑅₁ “ On)⟶On
31		frn 6712	. . . . . . . 8 ⊢ (rank:∪ (𝑅₁ “ On)⟶On → ran rank ⊆ On)
32	30, 31	ax-mp 5	. . . . . . 7 ⊢ ran rank ⊆ On
33	29, 32	sstri 3968	. . . . . 6 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) ⊆ On
34		hsmexlem4.u	. . . . . . . . . 10 ⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω))
35	34	ituni0 10430	. . . . . . . . 9 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘∅) = 𝑑)
36	35	elv 3464	. . . . . . . 8 ⊢ ((𝑈‘𝑑)‘∅) = 𝑑
37	36	imaeq2i 6045	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) = (rank “ 𝑑)
38		ffun 6708	. . . . . . . . . 10 ⊢ (rank:∪ (𝑅₁ “ On)⟶On → Fun rank)
39	30, 38	ax-mp 5	. . . . . . . . 9 ⊢ Fun rank
40		vex 3463	. . . . . . . . 9 ⊢ 𝑑 ∈ V
41		wdomimag 9599	. . . . . . . . 9 ⊢ ((Fun rank ∧ 𝑑 ∈ V) → (rank “ 𝑑) ≼^* 𝑑)
42	39, 40, 41	mp2an 692	. . . . . . . 8 ⊢ (rank “ 𝑑) ≼^* 𝑑
43		sneq 4611	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑})
44	43	fveq2d 6879	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (TC‘{𝑎}) = (TC‘{𝑑}))
45	44	raleqdv 3305	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
46		hsmexlem4.s	. . . . . . . . . . 11 ⊢ 𝑆 = {𝑎 ∈ ∪ (𝑅₁ “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋}
47	45, 46	elrab2 3674	. . . . . . . . . 10 ⊢ (𝑑 ∈ 𝑆 ↔ (𝑑 ∈ ∪ (𝑅₁ “ On) ∧ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
48	47	simprbi 496	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝑆 → ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋)
49		vsnex 5404	. . . . . . . . . . . 12 ⊢ {𝑑} ∈ V
50		tcid 9751	. . . . . . . . . . . 12 ⊢ ({𝑑} ∈ V → {𝑑} ⊆ (TC‘{𝑑}))
51	49, 50	ax-mp 5	. . . . . . . . . . 11 ⊢ {𝑑} ⊆ (TC‘{𝑑})
52		vsnid 4639	. . . . . . . . . . 11 ⊢ 𝑑 ∈ {𝑑}
53	51, 52	sselii 3955	. . . . . . . . . 10 ⊢ 𝑑 ∈ (TC‘{𝑑})
54		breq1 5122	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ≼ 𝑋 ↔ 𝑑 ≼ 𝑋))
55	54	rspcv 3597	. . . . . . . . . 10 ⊢ (𝑑 ∈ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋))
56	53, 55	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋)
57		domwdom 9586	. . . . . . . . 9 ⊢ (𝑑 ≼ 𝑋 → 𝑑 ≼^* 𝑋)
58	48, 56, 57	3syl 18	. . . . . . . 8 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ≼^* 𝑋)
59		wdomtr 9587	. . . . . . . 8 ⊢ (((rank “ 𝑑) ≼^* 𝑑 ∧ 𝑑 ≼^* 𝑋) → (rank “ 𝑑) ≼^* 𝑋)
60	42, 58, 59	sylancr 587	. . . . . . 7 ⊢ (𝑑 ∈ 𝑆 → (rank “ 𝑑) ≼^* 𝑋)
61	37, 60	eqbrtrid 5154	. . . . . 6 ⊢ (𝑑 ∈ 𝑆 → (rank “ ((𝑈‘𝑑)‘∅)) ≼^* 𝑋)
62		eqid 2735	. . . . . . 7 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅)))
63	62	hsmexlem1 10438	. . . . . 6 ⊢ (((rank “ ((𝑈‘𝑑)‘∅)) ⊆ On ∧ (rank “ ((𝑈‘𝑑)‘∅)) ≼^* 𝑋) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
64	33, 61, 63	sylancr 587	. . . . 5 ⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
65		hsmexlem4.h	. . . . . 6 ⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω)
66	65	hsmexlem7 10435	. . . . 5 ⊢ (𝐻‘∅) = (har‘𝒫 𝑋)
67	64, 66	eleqtrrdi 2845	. . . 4 ⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅))
68	67	rgen 3053	. . 3 ⊢ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)
69		nfra1 3266	. . . . . 6 ⊢ Ⅎ𝑑∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)
70		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑑 𝑒 ∈ ω
71	69, 70	nfan 1899	. . . . 5 ⊢ Ⅎ𝑑(∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω)
72	34	ituniiun 10434	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
73	72	elv 3464	. . . . . . . . . . . 12 ⊢ ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)
74	73	imaeq2i 6045	. . . . . . . . . . 11 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
75		imaiun 7236	. . . . . . . . . . 11 ⊢ (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
76	74, 75	eqtri 2758	. . . . . . . . . 10 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
77		oieq2 9525	. . . . . . . . . 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 5884	. . . . . . . 8 ⊢ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
80	58	ad2antll 729	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → 𝑑 ≼^* 𝑋)
81	65	hsmexlem9 10437	. . . . . . . . . 10 ⊢ (𝑒 ∈ ω → (𝐻‘𝑒) ∈ On)
82	81	ad2antrl 728	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘𝑒) ∈ On)
83		fveq2 6875	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑓 → (𝑈‘𝑑) = (𝑈‘𝑓))
84	83	fveq1d 6877	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑓 → ((𝑈‘𝑑)‘𝑒) = ((𝑈‘𝑓)‘𝑒))
85	84	imaeq2d 6047	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑓 → (rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)))
86		oieq2 9525	. . . . . . . . . . . . . . 15 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
87	85, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑓 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
88	87	dmeqd 5885	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑓 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
89	88	eleq1d 2819	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑓 → (dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
90		simpll 766	. . . . . . . . . . . 12 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒))
91	46	ssrab3 4057	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 ⊆ ∪ (𝑅₁ “ On)
92	91	sseli 3954	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ∈ ∪ (𝑅₁ “ On))
93		r1elssi 9817	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ ∪ (𝑅₁ “ On) → 𝑑 ⊆ ∪ (𝑅₁ “ On))
94	92, 93	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ⊆ ∪ (𝑅₁ “ On))
95	94	sselda 3958	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ ∪ (𝑅₁ “ On))
96		snssi 4784	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ 𝑑 → {𝑓} ⊆ 𝑑)
97	40	tcss 9756	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑓} ⊆ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
99	49	tcel 9757	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ {𝑑} → (TC‘𝑑) ⊆ (TC‘{𝑑}))
100	52, 99	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘𝑑) ⊆ (TC‘{𝑑}))
101	98, 100	sstrd 3969	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘{𝑑}))
102		ssralv 4027	. . . . . . . . . . . . . . . . 17 ⊢ ((TC‘{𝑓}) ⊆ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
103	101, 102	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ 𝑑 → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
104	48, 103	mpan9 506	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋)
105		sneq 4611	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑓 → {𝑎} = {𝑓})
106	105	fveq2d 6879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑓 → (TC‘{𝑎}) = (TC‘{𝑓}))
107	106	raleqdv 3305	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑓 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
108	107, 46	elrab2 3674	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ ∪ (𝑅₁ “ On) ∧ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
109	95, 104, 108	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
110	109	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
111	110	adantll 714	. . . . . . . . . . . 12 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
112	89, 90, 111	rspcdva 3602	. . . . . . . . . . 11 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))
113		imassrn 6058	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ ran rank
114	113, 32	sstri 3968	. . . . . . . . . . . 12 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ On
115		fvex 6888	. . . . . . . . . . . . . . 15 ⊢ ((𝑈‘𝑓)‘𝑒) ∈ V
116	115	funimaex 6624	. . . . . . . . . . . . . 14 ⊢ (Fun rank → (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V)
117	39, 116	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V
118	117	elpw 4579	. . . . . . . . . . . 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 3132	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
122		eqid 2735	. . . . . . . . . 10 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒)))
123		eqid 2735	. . . . . . . . . 10 ⊢ OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
124	122, 123	hsmexlem3 10440	. . . . . . . . 9 ⊢ (((𝑑 ≼^* 𝑋 ∧ (𝐻‘𝑒) ∈ On) ∧ ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
125	80, 82, 121, 124	syl21anc 837	. . . . . . . 8 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
126	79, 125	eqeltrid 2838	. . . . . . 7 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
127	65	hsmexlem8 10436	. . . . . . . 8 ⊢ (𝑒 ∈ ω → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
128	127	ad2antrl 728	. . . . . . 7 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
129	126, 128	eleqtrrd 2837	. . . . . 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 3240	. . . 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 7893	. 2 ⊢ (𝑐 ∈ ω → ∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐))
134	133	r19.21bi 3234	1 ⊢ ((𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆) → dom 𝑂 ∈ (𝐻‘𝑐))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∀wral 3051 {crab 3415 Vcvv 3459 ⊆ wss 3926 ∅c0 4308 𝒫 cpw 4575 {csn 4601 ∪ cuni 4883 ∪ ciun 4967 class class class wbr 5119 ↦ cmpt 5201 E cep 5552 × cxp 5652 dom cdm 5654 ran crn 5655 ↾ cres 5656 “ cima 5657 Oncon0 6352 suc csuc 6354 Fun wfun 6524 ⟶wf 6526 ‘cfv 6530 ωcom 7859 reccrdg 8421 ≼ cdom 8955 OrdIsocoi 9521 harchar 9568 ≼^* cwdom 9576 TCctc 9748 𝑅₁cr1 9774 rankcrnk 9775

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7727 ax-inf2 9653

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6483 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537 df-fv 6538 df-isom 6539 df-riota 7360 df-ov 7406 df-om 7860 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-smo 8358 df-recs 8383 df-rdg 8422 df-en 8958 df-dom 8959 df-sdom 8960 df-oi 9522 df-har 9569 df-wdom 9577 df-tc 9749 df-r1 9776 df-rank 9777

This theorem is referenced by: hsmexlem5 10442

W3C validator