Metamath Proof Explorer

Theorem noinfcbv

Description: Change bound variables for surreal infimum. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfcbv.1 ⊢T=if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
Assertion noinfcbv ⊢T=if∃a∈B∀b∈B¬b<saιa∈B|∀b∈B¬b<sa∪dom⁡ιa∈B|∀b∈B¬b<sa1𝑜c∈b|∃d∈Bb∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b⟼ιa|∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a

Proof

Step Hyp Ref Expression
1 noinfcbv.1 ⊢T=if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x
2 breq2 ⊢x=a→y<sx↔y<sa
3 2 notbid ⊢x=a→¬y<sx↔¬y<sa
4 3 ralbidv ⊢x=a→∀y∈B¬y<sx↔∀y∈B¬y<sa
5 breq1 ⊢y=b→y<sa↔b<sa
6 5 notbid ⊢y=b→¬y<sa↔¬b<sa
7 6 cbvralvw ⊢∀y∈B¬y<sa↔∀b∈B¬b<sa
8 4 7 bitrdi ⊢x=a→∀y∈B¬y<sx↔∀b∈B¬b<sa
9 8 cbvrexvw ⊢∃x∈B∀y∈B¬y<sx↔∃a∈B∀b∈B¬b<sa
10 8 cbvriotavw ⊢ιx∈B|∀y∈B¬y<sx=ιa∈B|∀b∈B¬b<sa
11 10 dmeqi ⊢dom⁡ιx∈B|∀y∈B¬y<sx=dom⁡ιa∈B|∀b∈B¬b<sa
12 11 opeq1i ⊢dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=dom⁡ιa∈B|∀b∈B¬b<sa1𝑜
13 12 sneqi ⊢dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=dom⁡ιa∈B|∀b∈B¬b<sa1𝑜
14 10 13 uneq12i ⊢ιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜=ιa∈B|∀b∈B¬b<sa∪dom⁡ιa∈B|∀b∈B¬b<sa1𝑜
15 eleq1w ⊢g=c→g∈dom⁡u↔c∈dom⁡u
16 suceq ⊢g=c→suc⁡g=suc⁡c
17 16 reseq2d ⊢g=c→u↾suc⁡g=u↾suc⁡c
18 16 reseq2d ⊢g=c→v↾suc⁡g=v↾suc⁡c
19 17 18 eqeq12d ⊢g=c→u↾suc⁡g=v↾suc⁡g↔u↾suc⁡c=v↾suc⁡c
20 19 imbi2d ⊢g=c→¬u<sv→u↾suc⁡g=v↾suc⁡g↔¬u<sv→u↾suc⁡c=v↾suc⁡c
21 20 ralbidv ⊢g=c→∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g↔∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c
22 fveqeq2 ⊢g=c→u⁡g=x↔u⁡c=x
23 15 21 22 3anbi123d ⊢g=c→g∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x↔c∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=x
24 23 rexbidv ⊢g=c→∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x↔∃u∈Bc∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=x
25 24 iotabidv ⊢g=c→ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=ιx|∃u∈Bc∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=x
26 eqeq2 ⊢x=a→u⁡c=x↔u⁡c=a
27 26 3anbi3d ⊢x=a→c∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=x↔c∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=a
28 27 rexbidv ⊢x=a→∃u∈Bc∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=x↔∃u∈Bc∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=a
29 dmeq ⊢u=d→dom⁡u=dom⁡d
30 29 eleq2d ⊢u=d→c∈dom⁡u↔c∈dom⁡d
31 breq1 ⊢u=d→u<sv↔d<sv
32 31 notbid ⊢u=d→¬u<sv↔¬d<sv
33 reseq1 ⊢u=d→u↾suc⁡c=d↾suc⁡c
34 33 eqeq1d ⊢u=d→u↾suc⁡c=v↾suc⁡c↔d↾suc⁡c=v↾suc⁡c
35 32 34 imbi12d ⊢u=d→¬u<sv→u↾suc⁡c=v↾suc⁡c↔¬d<sv→d↾suc⁡c=v↾suc⁡c
36 35 ralbidv ⊢u=d→∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c↔∀v∈B¬d<sv→d↾suc⁡c=v↾suc⁡c
37 breq2 ⊢v=e→d<sv↔d<se
38 37 notbid ⊢v=e→¬d<sv↔¬d<se
39 reseq1 ⊢v=e→v↾suc⁡c=e↾suc⁡c
40 39 eqeq2d ⊢v=e→d↾suc⁡c=v↾suc⁡c↔d↾suc⁡c=e↾suc⁡c
41 38 40 imbi12d ⊢v=e→¬d<sv→d↾suc⁡c=v↾suc⁡c↔¬d<se→d↾suc⁡c=e↾suc⁡c
42 41 cbvralvw ⊢∀v∈B¬d<sv→d↾suc⁡c=v↾suc⁡c↔∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c
43 36 42 bitrdi ⊢u=d→∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c↔∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c
44 fveq1 ⊢u=d→u⁡c=d⁡c
45 44 eqeq1d ⊢u=d→u⁡c=a↔d⁡c=a
46 30 43 45 3anbi123d ⊢u=d→c∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=a↔c∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a
47 46 cbvrexvw ⊢∃u∈Bc∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=a↔∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a
48 28 47 bitrdi ⊢x=a→∃u∈Bc∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=x↔∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a
49 48 cbviotavw ⊢ιx|∃u∈Bc∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡c=v↾suc⁡c∧u⁡c=x=ιa|∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a
50 25 49 eqtrdi ⊢g=c→ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=ιa|∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a
51 50 cbvmptv ⊢g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=c∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιa|∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a
52 eleq1w ⊢y=b→y∈dom⁡u↔b∈dom⁡u
53 suceq ⊢y=b→suc⁡y=suc⁡b
54 53 reseq2d ⊢y=b→u↾suc⁡y=u↾suc⁡b
55 53 reseq2d ⊢y=b→v↾suc⁡y=v↾suc⁡b
56 54 55 eqeq12d ⊢y=b→u↾suc⁡y=v↾suc⁡y↔u↾suc⁡b=v↾suc⁡b
57 56 imbi2d ⊢y=b→¬u<sv→u↾suc⁡y=v↾suc⁡y↔¬u<sv→u↾suc⁡b=v↾suc⁡b
58 57 ralbidv ⊢y=b→∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b
59 52 58 anbi12d ⊢y=b→y∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔b∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b
60 59 rexbidv ⊢y=b→∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∃u∈Bb∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b
61 29 eleq2d ⊢u=d→b∈dom⁡u↔b∈dom⁡d
62 reseq1 ⊢u=d→u↾suc⁡b=d↾suc⁡b
63 62 eqeq1d ⊢u=d→u↾suc⁡b=v↾suc⁡b↔d↾suc⁡b=v↾suc⁡b
64 32 63 imbi12d ⊢u=d→¬u<sv→u↾suc⁡b=v↾suc⁡b↔¬d<sv→d↾suc⁡b=v↾suc⁡b
65 64 ralbidv ⊢u=d→∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b↔∀v∈B¬d<sv→d↾suc⁡b=v↾suc⁡b
66 reseq1 ⊢v=e→v↾suc⁡b=e↾suc⁡b
67 66 eqeq2d ⊢v=e→d↾suc⁡b=v↾suc⁡b↔d↾suc⁡b=e↾suc⁡b
68 38 67 imbi12d ⊢v=e→¬d<sv→d↾suc⁡b=v↾suc⁡b↔¬d<se→d↾suc⁡b=e↾suc⁡b
69 68 cbvralvw ⊢∀v∈B¬d<sv→d↾suc⁡b=v↾suc⁡b↔∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b
70 65 69 bitrdi ⊢u=d→∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b↔∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b
71 61 70 anbi12d ⊢u=d→b∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b↔b∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b
72 71 cbvrexvw ⊢∃u∈Bb∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡b=v↾suc⁡b↔∃d∈Bb∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b
73 60 72 bitrdi ⊢y=b→∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y↔∃d∈Bb∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b
74 73 cbvabv ⊢y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y=b|∃d∈Bb∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b
75 74 mpteq1i ⊢c∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιa|∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a=c∈b|∃d∈Bb∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b⟼ιa|∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a
76 51 75 eqtri ⊢g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=c∈b|∃d∈Bb∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b⟼ιa|∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a
77 9 14 76 ifbieq12i ⊢if∃x∈B∀y∈B¬y<sxιx∈B|∀y∈B¬y<sx∪dom⁡ιx∈B|∀y∈B¬y<sx1𝑜g∈y|∃u∈By∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡y=v↾suc⁡y⟼ιx|∃u∈Bg∈dom⁡u∧∀v∈B¬u<sv→u↾suc⁡g=v↾suc⁡g∧u⁡g=x=if∃a∈B∀b∈B¬b<saιa∈B|∀b∈B¬b<sa∪dom⁡ιa∈B|∀b∈B¬b<sa1𝑜c∈b|∃d∈Bb∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b⟼ιa|∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a
78 1 77 eqtri ⊢T=if∃a∈B∀b∈B¬b<saιa∈B|∀b∈B¬b<sa∪dom⁡ιa∈B|∀b∈B¬b<sa1𝑜c∈b|∃d∈Bb∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡b=e↾suc⁡b⟼ιa|∃d∈Bc∈dom⁡d∧∀e∈B¬d<se→d↾suc⁡c=e↾suc⁡c∧d⁡c=a