Metamath Proof Explorer

Theorem dfac12lem1

Description: Lemma for dfac12 . (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Hypotheses dfac12.1 ⊢φ→A∈On
dfac12.3 ⊢φ→F:𝒫har⁡R1⁡A⟶1-1On
dfac12.4 ⊢G=recs⁡x∈V⟼y∈R1⁡dom⁡x⟼ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy
dfac12.5 ⊢φ→C∈On
dfac12.h ⊢H=OrdIsoEran⁡G⁡⋃C-1∘G⁡⋃C
Assertion dfac12lem1 ⊢φ→G⁡C=y∈R1⁡C⟼ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G⁡suc⁡rank⁡y⁡yF⁡Hy

Proof

Step Hyp Ref Expression
1 dfac12.1 ⊢φ→A∈On
2 dfac12.3 ⊢φ→F:𝒫har⁡R1⁡A⟶1-1On
3 dfac12.4 ⊢G=recs⁡x∈V⟼y∈R1⁡dom⁡x⟼ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy
4 dfac12.5 ⊢φ→C∈On
5 dfac12.h ⊢H=OrdIsoEran⁡G⁡⋃C-1∘G⁡⋃C
6 3 tfr2 ⊢C∈On→G⁡C=x∈V⟼y∈R1⁡dom⁡x⟼ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy⁡G↾C
7 4 6 syl ⊢φ→G⁡C=x∈V⟼y∈R1⁡dom⁡x⟼ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy⁡G↾C
8 3 tfr1 ⊢GFnOn
9 fnfun ⊢GFnOn→Fun⁡G
10 8 9 ax-mp ⊢Fun⁡G
11 resfunexg ⊢Fun⁡G∧C∈On→G↾C∈V
12 10 4 11 sylancr ⊢φ→G↾C∈V
13 dmeq ⊢x=G↾C→dom⁡x=dom⁡G↾C
14 13 fveq2d ⊢x=G↾C→R1⁡dom⁡x=R1⁡dom⁡G↾C
15 13 unieqd ⊢x=G↾C→⋃dom⁡x=⋃dom⁡G↾C
16 13 15 eqeq12d ⊢x=G↾C→dom⁡x=⋃dom⁡x↔dom⁡G↾C=⋃dom⁡G↾C
17 rneq ⊢x=G↾C→ran⁡x=ran⁡G↾C
18 df-ima ⊢GC=ran⁡G↾C
19 17 18 eqtr4di ⊢x=G↾C→ran⁡x=GC
20 19 unieqd ⊢x=G↾C→⋃ran⁡x=⋃GC
21 20 rneqd ⊢x=G↾C→ran⁡⋃ran⁡x=ran⁡⋃GC
22 21 unieqd ⊢x=G↾C→⋃ran⁡⋃ran⁡x=⋃ran⁡⋃GC
23 suceq ⊢⋃ran⁡⋃ran⁡x=⋃ran⁡⋃GC→suc⁡⋃ran⁡⋃ran⁡x=suc⁡⋃ran⁡⋃GC
24 22 23 syl ⊢x=G↾C→suc⁡⋃ran⁡⋃ran⁡x=suc⁡⋃ran⁡⋃GC
25 24 oveq1d ⊢x=G↾C→suc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y=suc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y
26 fveq1 ⊢x=G↾C→x⁡suc⁡rank⁡y=G↾C⁡suc⁡rank⁡y
27 26 fveq1d ⊢x=G↾C→x⁡suc⁡rank⁡y⁡y=G↾C⁡suc⁡rank⁡y⁡y
28 25 27 oveq12d ⊢x=G↾C→suc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡y=suc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡y
29 id ⊢x=G↾C→x=G↾C
30 29 15 fveq12d ⊢x=G↾C→x⁡⋃dom⁡x=G↾C⁡⋃dom⁡G↾C
31 30 rneqd ⊢x=G↾C→ran⁡x⁡⋃dom⁡x=ran⁡G↾C⁡⋃dom⁡G↾C
32 oieq2 ⊢ran⁡x⁡⋃dom⁡x=ran⁡G↾C⁡⋃dom⁡G↾C→OrdIsoEran⁡x⁡⋃dom⁡x=OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C
33 31 32 syl ⊢x=G↾C→OrdIsoEran⁡x⁡⋃dom⁡x=OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C
34 33 cnveqd ⊢x=G↾C→OrdIsoEran⁡x⁡⋃dom⁡x-1=OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1
35 34 30 coeq12d ⊢x=G↾C→OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡x=OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾C
36 35 imaeq1d ⊢x=G↾C→OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy=OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy
37 36 fveq2d ⊢x=G↾C→F⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy=F⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy
38 16 28 37 ifbieq12d ⊢x=G↾C→ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy=ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy
39 14 38 mpteq12dv ⊢x=G↾C→y∈R1⁡dom⁡x⟼ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy=y∈R1⁡dom⁡G↾C⟼ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy
40 eqid ⊢x∈V⟼y∈R1⁡dom⁡x⟼ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy=x∈V⟼y∈R1⁡dom⁡x⟼ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy
41 fvex ⊢R1⁡dom⁡G↾C∈V
42 41 mptex ⊢y∈R1⁡dom⁡G↾C⟼ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy∈V
43 39 40 42 fvmpt ⊢G↾C∈V→x∈V⟼y∈R1⁡dom⁡x⟼ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy⁡G↾C=y∈R1⁡dom⁡G↾C⟼ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy
44 12 43 syl ⊢φ→x∈V⟼y∈R1⁡dom⁡x⟼ifdom⁡x=⋃dom⁡xsuc⁡⋃ran⁡⋃ran⁡x⋅𝑜rank⁡y+𝑜x⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡x⁡⋃dom⁡x-1∘x⁡⋃dom⁡xy⁡G↾C=y∈R1⁡dom⁡G↾C⟼ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy
45 onss ⊢C∈On→C⊆On
46 4 45 syl ⊢φ→C⊆On
47 fnssres ⊢GFnOn∧C⊆On→G↾CFnC
48 8 46 47 sylancr ⊢φ→G↾CFnC
49 48 fndmd ⊢φ→dom⁡G↾C=C
50 49 fveq2d ⊢φ→R1⁡dom⁡G↾C=R1⁡C
51 50 mpteq1d ⊢φ→y∈R1⁡dom⁡G↾C⟼ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy=y∈R1⁡C⟼ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy
52 49 adantr ⊢φ∧y∈R1⁡C→dom⁡G↾C=C
53 52 unieqd ⊢φ∧y∈R1⁡C→⋃dom⁡G↾C=⋃C
54 52 53 eqeq12d ⊢φ∧y∈R1⁡C→dom⁡G↾C=⋃dom⁡G↾C↔C=⋃C
55 54 ifbid ⊢φ∧y∈R1⁡C→ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy=ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy
56 rankr1ai ⊢y∈R1⁡C→rank⁡y∈C
57 56 ad2antlr ⊢φ∧y∈R1⁡C∧C=⋃C→rank⁡y∈C
58 simpr ⊢φ∧y∈R1⁡C∧C=⋃C→C=⋃C
59 57 58 eleqtrd ⊢φ∧y∈R1⁡C∧C=⋃C→rank⁡y∈⋃C
60 eloni ⊢C∈On→Ord⁡C
61 ordsucuniel ⊢Ord⁡C→rank⁡y∈⋃C↔suc⁡rank⁡y∈C
62 4 60 61 3syl ⊢φ→rank⁡y∈⋃C↔suc⁡rank⁡y∈C
63 62 ad2antrr ⊢φ∧y∈R1⁡C∧C=⋃C→rank⁡y∈⋃C↔suc⁡rank⁡y∈C
64 59 63 mpbid ⊢φ∧y∈R1⁡C∧C=⋃C→suc⁡rank⁡y∈C
65 64 fvresd ⊢φ∧y∈R1⁡C∧C=⋃C→G↾C⁡suc⁡rank⁡y=G⁡suc⁡rank⁡y
66 65 fveq1d ⊢φ∧y∈R1⁡C∧C=⋃C→G↾C⁡suc⁡rank⁡y⁡y=G⁡suc⁡rank⁡y⁡y
67 66 oveq2d ⊢φ∧y∈R1⁡C∧C=⋃C→suc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡y=suc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G⁡suc⁡rank⁡y⁡y
68 67 ifeq1da ⊢φ∧y∈R1⁡C→ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy=ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy
69 53 adantr ⊢φ∧y∈R1⁡C∧¬C=⋃C→⋃dom⁡G↾C=⋃C
70 69 fveq2d ⊢φ∧y∈R1⁡C∧¬C=⋃C→G↾C⁡⋃dom⁡G↾C=G↾C⁡⋃C
71 4 ad2antrr ⊢φ∧y∈R1⁡C∧¬C=⋃C→C∈On
72 uniexg ⊢C∈On→⋃C∈V
73 sucidg ⊢⋃C∈V→⋃C∈suc⁡⋃C
74 71 72 73 3syl ⊢φ∧y∈R1⁡C∧¬C=⋃C→⋃C∈suc⁡⋃C
75 4 adantr ⊢φ∧y∈R1⁡C→C∈On
76 orduniorsuc ⊢Ord⁡C→C=⋃C∨C=suc⁡⋃C
77 75 60 76 3syl ⊢φ∧y∈R1⁡C→C=⋃C∨C=suc⁡⋃C
78 77 orcanai ⊢φ∧y∈R1⁡C∧¬C=⋃C→C=suc⁡⋃C
79 74 78 eleqtrrd ⊢φ∧y∈R1⁡C∧¬C=⋃C→⋃C∈C
80 79 fvresd ⊢φ∧y∈R1⁡C∧¬C=⋃C→G↾C⁡⋃C=G⁡⋃C
81 70 80 eqtrd ⊢φ∧y∈R1⁡C∧¬C=⋃C→G↾C⁡⋃dom⁡G↾C=G⁡⋃C
82 81 rneqd ⊢φ∧y∈R1⁡C∧¬C=⋃C→ran⁡G↾C⁡⋃dom⁡G↾C=ran⁡G⁡⋃C
83 oieq2 ⊢ran⁡G↾C⁡⋃dom⁡G↾C=ran⁡G⁡⋃C→OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C=OrdIsoEran⁡G⁡⋃C
84 82 83 syl ⊢φ∧y∈R1⁡C∧¬C=⋃C→OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C=OrdIsoEran⁡G⁡⋃C
85 84 cnveqd ⊢φ∧y∈R1⁡C∧¬C=⋃C→OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1=OrdIsoEran⁡G⁡⋃C-1
86 85 81 coeq12d ⊢φ∧y∈R1⁡C∧¬C=⋃C→OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾C=OrdIsoEran⁡G⁡⋃C-1∘G⁡⋃C
87 86 5 eqtr4di ⊢φ∧y∈R1⁡C∧¬C=⋃C→OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾C=H
88 87 imaeq1d ⊢φ∧y∈R1⁡C∧¬C=⋃C→OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy=Hy
89 88 fveq2d ⊢φ∧y∈R1⁡C∧¬C=⋃C→F⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy=F⁡Hy
90 89 ifeq2da ⊢φ∧y∈R1⁡C→ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy=ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G⁡suc⁡rank⁡y⁡yF⁡Hy
91 55 68 90 3eqtrd ⊢φ∧y∈R1⁡C→ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy=ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G⁡suc⁡rank⁡y⁡yF⁡Hy
92 91 mpteq2dva ⊢φ→y∈R1⁡C⟼ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy=y∈R1⁡C⟼ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G⁡suc⁡rank⁡y⁡yF⁡Hy
93 51 92 eqtrd ⊢φ→y∈R1⁡dom⁡G↾C⟼ifdom⁡G↾C=⋃dom⁡G↾Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G↾C⁡suc⁡rank⁡y⁡yF⁡OrdIsoEran⁡G↾C⁡⋃dom⁡G↾C-1∘G↾C⁡⋃dom⁡G↾Cy=y∈R1⁡C⟼ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G⁡suc⁡rank⁡y⁡yF⁡Hy
94 7 44 93 3eqtrd ⊢φ→G⁡C=y∈R1⁡C⟼ifC=⋃Csuc⁡⋃ran⁡⋃GC⋅𝑜rank⁡y+𝑜G⁡suc⁡rank⁡y⁡yF⁡Hy