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 10546

Description: Lemma for hsmex 10549. 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 6916	. . . . . . . . 9 ⊢ (𝑐 = ∅ → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘∅))
3	2	imaeq2d 6070	. . . . . . . 8 ⊢ (𝑐 = ∅ → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘∅)))
4		oieq2 9544	. . . . . . . 8 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘∅)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
5	3, 4	syl 18	. . . . . . 7 ⊢ (𝑐 = ∅ → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
6	1, 5	eqtrid 2810	. . . . . 6 ⊢ (𝑐 = ∅ → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
7	6	dmeqd 5899	. . . . 5 ⊢ (𝑐 = ∅ → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))))
8		fveq2 6916	. . . . 5 ⊢ (𝑐 = ∅ → (𝐻‘𝑐) = (𝐻‘∅))
9	7, 8	eleq12d 2858	. . . 4 ⊢ (𝑐 = ∅ → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
10	9	ralbidv 3189	. . 3 ⊢ (𝑐 = ∅ → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)))
11		fveq2 6916	. . . . . . . . 9 ⊢ (𝑐 = 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘𝑒))
12	11	imaeq2d 6070	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘𝑒)))
13		oieq2 9544	. . . . . . . 8 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
14	12, 13	syl 18	. . . . . . 7 ⊢ (𝑐 = 𝑒 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
15	1, 14	eqtrid 2810	. . . . . 6 ⊢ (𝑐 = 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
16	15	dmeqd 5899	. . . . 5 ⊢ (𝑐 = 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))))
17		fveq2 6916	. . . . 5 ⊢ (𝑐 = 𝑒 → (𝐻‘𝑐) = (𝐻‘𝑒))
18	16, 17	eleq12d 2858	. . . 4 ⊢ (𝑐 = 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
19	18	ralbidv 3189	. . 3 ⊢ (𝑐 = 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)))
20		fveq2 6916	. . . . . . . . 9 ⊢ (𝑐 = suc 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘suc 𝑒))
21	20	imaeq2d 6070	. . . . . . . 8 ⊢ (𝑐 = suc 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘suc 𝑒)))
22		oieq2 9544	. . . . . . . 8 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘suc 𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
23	21, 22	syl 18	. . . . . . 7 ⊢ (𝑐 = suc 𝑒 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
24	1, 23	eqtrid 2810	. . . . . 6 ⊢ (𝑐 = suc 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
25	24	dmeqd 5899	. . . . 5 ⊢ (𝑐 = suc 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))))
26		fveq2 6916	. . . . 5 ⊢ (𝑐 = suc 𝑒 → (𝐻‘𝑐) = (𝐻‘suc 𝑒))
27	25, 26	eleq12d 2858	. . . 4 ⊢ (𝑐 = suc 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
28	27	ralbidv 3189	. . 3 ⊢ (𝑐 = suc 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
29		imassrn 6216	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) ⊆ ran rank
30		rankf 9839	. . . . . . . 8 ⊢ rank:∪ (𝑅₁ “ On)⟶On
31		frn 6747	. . . . . . . 8 ⊢ (rank:∪ (𝑅₁ “ On)⟶On → ran rank ⊆ On)
32	30, 31	ax-mp 5	. . . . . . 7 ⊢ ran rank ⊆ On
33	29, 32	sstri 3922	. . . . . 6 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) ⊆ On
34		hsmexlem4.u	. . . . . . . . . 10 ⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω))
35	34	ituni0 10535	. . . . . . . . 9 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘∅) = 𝑑)
36	35	elv 3459	. . . . . . . 8 ⊢ ((𝑈‘𝑑)‘∅) = 𝑑
37	36	imaeq2i 6068	. . . . . . 7 ⊢ (rank “ ((𝑈‘𝑑)‘∅)) = (rank “ 𝑑)
38		ffun 6742	. . . . . . . . . 10 ⊢ (rank:∪ (𝑅₁ “ On)⟶On → Fun rank)
39	30, 38	ax-mp 5	. . . . . . . . 9 ⊢ Fun rank
40		vex 3458	. . . . . . . . 9 ⊢ 𝑑 ∈ V
41		wdomimag 9618	. . . . . . . . 9 ⊢ ((Fun rank ∧ 𝑑 ∈ V) → (rank “ 𝑑) ≼^* 𝑑)
42	39, 40, 41	mp2an 705	. . . . . . . 8 ⊢ (rank “ 𝑑) ≼^* 𝑑
43		sneq 4594	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑})
44	43	fveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (TC‘{𝑎}) = (TC‘{𝑑}))
45	44	raleqdv 3323	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
46		hsmexlem4.s	. . . . . . . . . . 11 ⊢ 𝑆 = {𝑎 ∈ ∪ (𝑅₁ “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋}
47	45, 46	elrab2 3652	. . . . . . . . . 10 ⊢ (𝑑 ∈ 𝑆 ↔ (𝑑 ∈ ∪ (𝑅₁ “ On) ∧ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋))
48	47	simprbi 503	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝑆 → ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋)
49		vsnex 5400	. . . . . . . . . . . 12 ⊢ {𝑑} ∈ V
50		tcid 9775	. . . . . . . . . . . 12 ⊢ ({𝑑} ∈ V → {𝑑} ⊆ (TC‘{𝑑}))
51	49, 50	ax-mp 5	. . . . . . . . . . 11 ⊢ {𝑑} ⊆ (TC‘{𝑑})
52		vsnid 4625	. . . . . . . . . . 11 ⊢ 𝑑 ∈ {𝑑}
53	51, 52	sselii 3910	. . . . . . . . . 10 ⊢ 𝑑 ∈ (TC‘{𝑑})
54		breq1 5111	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝑏 ≼ 𝑋 ↔ 𝑑 ≼ 𝑋))
55	54	rspcv 3576	. . . . . . . . . 10 ⊢ (𝑑 ∈ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋))
56	53, 55	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋)
57		domwdom 9605	. . . . . . . . 9 ⊢ (𝑑 ≼ 𝑋 → 𝑑 ≼^* 𝑋)
58	48, 56, 57	3syl 19	. . . . . . . 8 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ≼^* 𝑋)
59		wdomtr 9606	. . . . . . . 8 ⊢ (((rank “ 𝑑) ≼^* 𝑑 ∧ 𝑑 ≼^* 𝑋) → (rank “ 𝑑) ≼^* 𝑋)
60	42, 58, 59	sylancr 599	. . . . . . 7 ⊢ (𝑑 ∈ 𝑆 → (rank “ 𝑑) ≼^* 𝑋)
61	37, 60	eqbrtrid 5146	. . . . . 6 ⊢ (𝑑 ∈ 𝑆 → (rank “ ((𝑈‘𝑑)‘∅)) ≼^* 𝑋)
62		eqid 2763	. . . . . . 7 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅)))
63	62	hsmexlem1 10543	. . . . . 6 ⊢ (((rank “ ((𝑈‘𝑑)‘∅)) ⊆ On ∧ (rank “ ((𝑈‘𝑑)‘∅)) ≼^* 𝑋) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
64	33, 61, 63	sylancr 599	. . . . 5 ⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
65		hsmexlem4.h	. . . . . 6 ⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω)
66	65	hsmexlem7 10540	. . . . 5 ⊢ (𝐻‘∅) = (har‘𝒫 𝑋)
67	64, 66	eleqtrrdi 2875	. . . 4 ⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅))
68	67	rgen 3082	. . 3 ⊢ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)
69		nfra1 3290	. . . . . 6 ⊢ Ⅎ𝑑∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)
70		nfv 1949	. . . . . 6 ⊢ Ⅎ𝑑 𝑒 ∈ ω
71	69, 70	nfan 1934	. . . . 5 ⊢ Ⅎ𝑑(∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω)
72	34	ituniiun 10539	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
73	72	elv 3459	. . . . . . . . . . . 12 ⊢ ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)
74	73	imaeq2i 6068	. . . . . . . . . . 11 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒))
75		imaiun 7280	. . . . . . . . . . 11 ⊢ (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
76	74, 75	eqtri 2786	. . . . . . . . . 10 ⊢ (rank “ ((𝑈‘𝑑)‘suc 𝑒)) = ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))
77		oieq2 9544	. . . . . . . . . 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 5898	. . . . . . . 8 ⊢ dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
80	58	ad2antll 742	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → 𝑑 ≼^* 𝑋)
81	65	hsmexlem9 10542	. . . . . . . . . 10 ⊢ (𝑒 ∈ ω → (𝐻‘𝑒) ∈ On)
82	81	ad2antrl 741	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘𝑒) ∈ On)
83		fveq2 6916	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑓 → (𝑈‘𝑑) = (𝑈‘𝑓))
84	83	fveq1d 6918	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑓 → ((𝑈‘𝑑)‘𝑒) = ((𝑈‘𝑓)‘𝑒))
85	84	imaeq2d 6070	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑓 → (rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)))
86		oieq2 9544	. . . . . . . . . . . . . . 15 ⊢ ((rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
87	85, 86	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑓 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
88	87	dmeqd 5899	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑓 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))))
89	88	eleq1d 2849	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑓 → (dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ↔ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
90		simpll 779	. . . . . . . . . . . 12 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒))
91	46	ssrab3 4010	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 ⊆ ∪ (𝑅₁ “ On)
92	91	sseli 3909	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ∈ ∪ (𝑅₁ “ On))
93		r1elssi 9850	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ ∪ (𝑅₁ “ On) → 𝑑 ⊆ ∪ (𝑅₁ “ On))
94	92, 93	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ 𝑆 → 𝑑 ⊆ ∪ (𝑅₁ “ On))
95	94	sselda 3913	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ ∪ (𝑅₁ “ On))
96		snssi 4748	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ 𝑑 → {𝑓} ⊆ 𝑑)
97	40	tcss 9780	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑓} ⊆ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
98	96, 97	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
99	49	tcel 9781	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ {𝑑} → (TC‘𝑑) ⊆ (TC‘{𝑑}))
100	52, 99	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ 𝑑 → (TC‘𝑑) ⊆ (TC‘{𝑑}))
101	98, 100	sstrd 3923	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘{𝑑}))
102		ssralv 3982	. . . . . . . . . . . . . . . . 17 ⊢ ((TC‘{𝑓}) ⊆ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
103	101, 102	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ 𝑑 → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
104	48, 103	mpan9 516	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋)
105		sneq 4594	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑓 → {𝑎} = {𝑓})
106	105	fveq2d 6920	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑓 → (TC‘{𝑎}) = (TC‘{𝑓}))
107	106	raleqdv 3323	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑓 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
108	107, 46	elrab2 3652	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ ∪ (𝑅₁ “ On) ∧ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋))
109	95, 104, 108	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
110	109	adantll 727	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
111	110	adantll 727	. . . . . . . . . . . 12 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆)
112	89, 90, 111	rspcdva 3581	. . . . . . . . . . 11 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))
113		imassrn 6216	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ ran rank
114	113, 32	sstri 3922	. . . . . . . . . . . 12 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ On
115		fvex 6929	. . . . . . . . . . . . . . 15 ⊢ ((𝑈‘𝑓)‘𝑒) ∈ V
116	115	funimaex 6657	. . . . . . . . . . . . . 14 ⊢ (Fun rank → (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V)
117	39, 116	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V
118	117	elpw 4564	. . . . . . . . . . . 12 ⊢ ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ↔ (rank “ ((𝑈‘𝑓)‘𝑒)) ⊆ On)
119	114, 118	mpbir 234	. . . . . . . . . . 11 ⊢ (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On
120	112, 119	jctil 529	. . . . . . . . . 10 ⊢ (((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
121	120	ralrimiva 3158	. . . . . . . . 9 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)))
122		eqid 2763	. . . . . . . . . 10 ⊢ OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒)))
123		eqid 2763	. . . . . . . . . 10 ⊢ OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))
124	122, 123	hsmexlem3 10545	. . . . . . . . 9 ⊢ (((𝑑 ≼^* 𝑋 ∧ (𝐻‘𝑒) ∈ On) ∧ ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
125	80, 82, 121, 124	syl21anc 851	. . . . . . . 8 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
126	79, 125	eqeltrid 2868	. . . . . . 7 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
127	65	hsmexlem8 10541	. . . . . . . 8 ⊢ (𝑒 ∈ ω → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
128	127	ad2antrl 741	. . . . . . 7 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒))))
129	126, 128	eleqtrrd 2867	. . . . . 6 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
130	129	expr 462	. . . . 5 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω) → (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
131	71, 130	ralrimi 3264	. . . 4 ⊢ ((∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
132	131	expcom 419	. . 3 ⊢ (𝑒 ∈ ω → (∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
133	10, 19, 28, 68, 132	finds1 7945	. 2 ⊢ (𝑐 ∈ ω → ∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐))
134	133	r19.21bi 3258	1 ⊢ ((𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆) → dom 𝑂 ∈ (𝐻‘𝑐))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∀wral 3080 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∅c0 4281 𝒫 cpw 4560 {csn 4588 ∪ cuni 4872 ∪ ciun 4956 class class class wbr 5108 ↦ cmpt 5192 E cep 5557 × cxp 5656 dom cdm 5658 ran crn 5659 ↾ cres 5660 “ cima 5661 Oncon0 6388 suc csuc 6390 Fun wfun 6560 ⟶wf 6562 ‘cfv 6566 ωcom 7911 reccrdg 8455 ≼ cdom 9009 OrdIsocoi 9540 harchar 9587 ≼^* cwdom 9595 TCctc 9772 𝑅₁cr1 9803 rankcrnk 9804

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-inf2 9679

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-smo 8392 df-recs 8417 df-rdg 8456 df-en 9012 df-dom 9013 df-sdom 9014 df-oi 9541 df-har 9588 df-wdom 9596 df-tc 9773 df-r1 9805 df-rank 9806

This theorem is used by: hsmexlem5 10547

W3C validator